%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUN076+2 : TPTP v8.1.0. Released v7.3.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n019.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 : Mon Jul 18 16:19:15 EDT 2022
% Result : Theorem 27.63s 28.00s
% Output : Refutation 27.63s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : NUN076+2 : TPTP v8.1.0. Released v7.3.0.
% 0.07/0.14 % Command : bliksem %s
% 0.13/0.35 % Computer : n019.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % DateTime : Thu Jun 2 10:48:10 EDT 2022
% 0.13/0.36 % CPUTime :
% 6.53/6.92 *** allocated 10000 integers for termspace/termends
% 6.53/6.92 *** allocated 10000 integers for clauses
% 6.53/6.92 *** allocated 10000 integers for justifications
% 6.53/6.92 Bliksem 1.12
% 6.53/6.92
% 6.53/6.92
% 6.53/6.92 Automatic Strategy Selection
% 6.53/6.92
% 6.53/6.92
% 6.53/6.92 Clauses:
% 6.53/6.92
% 6.53/6.92 { alpha1( skol1, X ), r1( X ) }.
% 6.53/6.92 { alpha1( skol1, X ), X = skol1 }.
% 6.53/6.92 { ! alpha1( X, Y ), ! r1( Y ) }.
% 6.53/6.92 { ! alpha1( X, Y ), ! Y = X }.
% 6.53/6.92 { r1( Y ), Y = X, alpha1( X, Y ) }.
% 6.53/6.92 { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 6.53/6.92 { alpha2( X, skol2( X ), Y ), Y = skol2( X ) }.
% 6.53/6.92 { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 6.53/6.92 { ! alpha2( X, Y, Z ), ! Z = Y }.
% 6.53/6.92 { r2( X, Z ), Z = Y, alpha2( X, Y, Z ) }.
% 6.53/6.92 { alpha3( X, Y, skol3( X, Y ), Z ), r3( X, Y, Z ) }.
% 6.53/6.92 { alpha3( X, Y, skol3( X, Y ), Z ), Z = skol3( X, Y ) }.
% 6.53/6.92 { ! alpha3( X, Y, Z, T ), ! r3( X, Y, T ) }.
% 6.53/6.92 { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 6.53/6.92 { r3( X, Y, T ), T = Z, alpha3( X, Y, Z, T ) }.
% 6.53/6.92 { alpha4( X, Y, skol4( X, Y ), Z ), r4( X, Y, Z ) }.
% 6.53/6.92 { alpha4( X, Y, skol4( X, Y ), Z ), Z = skol4( X, Y ) }.
% 6.53/6.92 { ! alpha4( X, Y, Z, T ), ! r4( X, Y, T ) }.
% 6.53/6.92 { ! alpha4( X, Y, Z, T ), ! T = Z }.
% 6.53/6.92 { r4( X, Y, T ), T = Z, alpha4( X, Y, Z, T ) }.
% 6.53/6.92 { r2( Y, skol16( Z, Y ) ) }.
% 6.53/6.92 { r3( X, skol16( X, Y ), skol11( X, Y ) ) }.
% 6.53/6.92 { skol11( X, Y ) = skol5( X, Y ) }.
% 6.53/6.92 { r2( skol19( X, Y ), skol5( X, Y ) ) }.
% 6.53/6.92 { r3( X, Y, skol19( X, Y ) ) }.
% 6.53/6.92 { r2( Y, skol17( Z, Y ) ) }.
% 6.53/6.92 { r4( X, skol17( X, Y ), skol12( X, Y ) ) }.
% 6.53/6.92 { skol12( X, Y ) = skol6( X, Y ) }.
% 6.53/6.92 { r3( skol20( X, Y ), X, skol6( X, Y ) ) }.
% 6.53/6.92 { r4( X, Y, skol20( X, Y ) ) }.
% 6.53/6.92 { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y }.
% 6.53/6.92 { r1( skol13( Y ) ) }.
% 6.53/6.92 { r3( X, skol13( X ), skol7( X ) ) }.
% 6.53/6.92 { skol7( X ) = X }.
% 6.53/6.92 { r1( skol14( Z ) ) }.
% 6.53/6.92 { skol8( Y ) = skol14( Y ) }.
% 6.53/6.92 { r1( skol18( Y ) ) }.
% 6.53/6.92 { r4( X, skol18( X ), skol8( X ) ) }.
% 6.53/6.92 { alpha5( X ), r2( skol15( Y ), skol9( Y ) ) }.
% 6.53/6.92 { alpha5( X ), X = skol9( X ) }.
% 6.53/6.92 { ! alpha5( X ), r1( skol10( Y ) ) }.
% 6.53/6.92 { ! alpha5( X ), X = skol10( X ) }.
% 6.53/6.92 { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 6.53/6.92 { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 6.53/6.92 { ! Z = X, ! r4( T, Y, Z ), ! r2( U, T ), ! r1( W ), ! r2( W, U ), ! r3( Y
% 6.53/6.92 , V1, V0 ), ! V0 = X }.
% 6.53/6.92
% 6.53/6.92 percentage equality = 0.279070, percentage horn = 0.688889
% 6.53/6.92 This is a problem with some equality
% 6.53/6.92
% 6.53/6.92
% 6.53/6.92
% 6.53/6.92 Options Used:
% 6.53/6.92
% 6.53/6.92 useres = 1
% 6.53/6.92 useparamod = 1
% 6.53/6.92 useeqrefl = 1
% 6.53/6.92 useeqfact = 1
% 6.53/6.92 usefactor = 1
% 6.53/6.92 usesimpsplitting = 0
% 6.53/6.92 usesimpdemod = 5
% 6.53/6.92 usesimpres = 3
% 6.53/6.92
% 6.53/6.92 resimpinuse = 1000
% 6.53/6.92 resimpclauses = 20000
% 6.53/6.92 substype = eqrewr
% 6.53/6.92 backwardsubs = 1
% 6.53/6.92 selectoldest = 5
% 6.53/6.92
% 6.53/6.92 litorderings [0] = split
% 6.53/6.92 litorderings [1] = extend the termordering, first sorting on arguments
% 6.53/6.92
% 6.53/6.92 termordering = kbo
% 6.53/6.92
% 6.53/6.92 litapriori = 0
% 6.53/6.92 termapriori = 1
% 6.53/6.92 litaposteriori = 0
% 6.53/6.92 termaposteriori = 0
% 6.53/6.92 demodaposteriori = 0
% 6.53/6.92 ordereqreflfact = 0
% 6.53/6.92
% 6.53/6.92 litselect = negord
% 6.53/6.92
% 6.53/6.92 maxweight = 15
% 6.53/6.92 maxdepth = 30000
% 6.53/6.92 maxlength = 115
% 6.53/6.92 maxnrvars = 195
% 6.53/6.92 excuselevel = 1
% 6.53/6.92 increasemaxweight = 1
% 6.53/6.92
% 6.53/6.92 maxselected = 10000000
% 6.53/6.92 maxnrclauses = 10000000
% 6.53/6.92
% 6.53/6.92 showgenerated = 0
% 6.53/6.92 showkept = 0
% 6.53/6.92 showselected = 0
% 6.53/6.92 showdeleted = 0
% 6.53/6.92 showresimp = 1
% 6.53/6.92 showstatus = 2000
% 6.53/6.92
% 6.53/6.92 prologoutput = 0
% 6.53/6.92 nrgoals = 5000000
% 6.53/6.92 totalproof = 1
% 6.53/6.92
% 6.53/6.92 Symbols occurring in the translation:
% 6.53/6.92
% 6.53/6.92 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 6.53/6.92 . [1, 2] (w:1, o:66, a:1, s:1, b:0),
% 6.53/6.92 ! [4, 1] (w:0, o:50, a:1, s:1, b:0),
% 6.53/6.92 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.53/6.92 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 6.53/6.92 r1 [37, 1] (w:1, o:55, a:1, s:1, b:0),
% 6.53/6.92 r2 [41, 2] (w:1, o:90, a:1, s:1, b:0),
% 6.53/6.92 r3 [46, 3] (w:1, o:102, a:1, s:1, b:0),
% 6.53/6.92 r4 [51, 3] (w:1, o:103, a:1, s:1, b:0),
% 6.53/6.92 alpha1 [82, 2] (w:1, o:91, a:1, s:1, b:1),
% 6.53/6.92 alpha2 [83, 3] (w:1, o:104, a:1, s:1, b:1),
% 6.53/6.92 alpha3 [84, 4] (w:1, o:105, a:1, s:1, b:1),
% 6.53/6.92 alpha4 [85, 4] (w:1, o:106, a:1, s:1, b:1),
% 6.53/6.92 alpha5 [86, 1] (w:1, o:56, a:1, s:1, b:1),
% 6.53/6.92 skol1 [87, 0] (w:1, o:49, a:1, s:1, b:1),
% 6.53/6.92 skol2 [88, 1] (w:1, o:62, a:1, s:1, b:1),
% 6.53/6.92 skol3 [89, 2] (w:1, o:93, a:1, s:1, b:1),
% 6.53/6.92 skol4 [90, 2] (w:1, o:94, a:1, s:1, b:1),
% 6.53/6.92 skol5 [91, 2] (w:1, o:95, a:1, s:1, b:1),
% 6.53/6.92 skol6 [92, 2] (w:1, o:96, a:1, s:1, b:1),
% 6.53/6.92 skol7 [93, 1] (w:1, o:63, a:1, s:1, b:1),
% 27.63/28.00 skol8 [94, 1] (w:1, o:64, a:1, s:1, b:1),
% 27.63/28.00 skol9 [95, 1] (w:1, o:65, a:1, s:1, b:1),
% 27.63/28.00 skol10 [96, 1] (w:1, o:57, a:1, s:1, b:1),
% 27.63/28.00 skol11 [97, 2] (w:1, o:97, a:1, s:1, b:1),
% 27.63/28.00 skol12 [98, 2] (w:1, o:98, a:1, s:1, b:1),
% 27.63/28.00 skol13 [99, 1] (w:1, o:58, a:1, s:1, b:1),
% 27.63/28.00 skol14 [100, 1] (w:1, o:59, a:1, s:1, b:1),
% 27.63/28.00 skol15 [101, 1] (w:1, o:60, a:1, s:1, b:1),
% 27.63/28.00 skol16 [102, 2] (w:1, o:99, a:1, s:1, b:1),
% 27.63/28.00 skol17 [103, 2] (w:1, o:100, a:1, s:1, b:1),
% 27.63/28.00 skol18 [104, 1] (w:1, o:61, a:1, s:1, b:1),
% 27.63/28.00 skol19 [105, 2] (w:1, o:101, a:1, s:1, b:1),
% 27.63/28.00 skol20 [106, 2] (w:1, o:92, a:1, s:1, b:1).
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Starting Search:
% 27.63/28.00
% 27.63/28.00 *** allocated 15000 integers for clauses
% 27.63/28.00 *** allocated 22500 integers for clauses
% 27.63/28.00 *** allocated 33750 integers for clauses
% 27.63/28.00 *** allocated 50625 integers for clauses
% 27.63/28.00 *** allocated 15000 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 75937 integers for clauses
% 27.63/28.00 *** allocated 22500 integers for termspace/termends
% 27.63/28.00 *** allocated 113905 integers for clauses
% 27.63/28.00 *** allocated 33750 integers for termspace/termends
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 7400
% 27.63/28.00 Kept: 2007
% 27.63/28.00 Inuse: 210
% 27.63/28.00 Deleted: 43
% 27.63/28.00 Deletedinuse: 25
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 170857 integers for clauses
% 27.63/28.00 *** allocated 50625 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 75937 integers for termspace/termends
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 16777
% 27.63/28.00 Kept: 4013
% 27.63/28.00 Inuse: 287
% 27.63/28.00 Deleted: 71
% 27.63/28.00 Deletedinuse: 44
% 27.63/28.00
% 27.63/28.00 *** allocated 256285 integers for clauses
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 113905 integers for termspace/termends
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 25416
% 27.63/28.00 Kept: 6036
% 27.63/28.00 Inuse: 344
% 27.63/28.00 Deleted: 85
% 27.63/28.00 Deletedinuse: 48
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 384427 integers for clauses
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 36996
% 27.63/28.00 Kept: 8039
% 27.63/28.00 Inuse: 419
% 27.63/28.00 Deleted: 104
% 27.63/28.00 Deletedinuse: 48
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 170857 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 576640 integers for clauses
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 45150
% 27.63/28.00 Kept: 10452
% 27.63/28.00 Inuse: 458
% 27.63/28.00 Deleted: 105
% 27.63/28.00 Deletedinuse: 49
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 56840
% 27.63/28.00 Kept: 12465
% 27.63/28.00 Inuse: 513
% 27.63/28.00 Deleted: 113
% 27.63/28.00 Deletedinuse: 49
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 256285 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 69260
% 27.63/28.00 Kept: 14483
% 27.63/28.00 Inuse: 573
% 27.63/28.00 Deleted: 120
% 27.63/28.00 Deletedinuse: 49
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 864960 integers for clauses
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 84329
% 27.63/28.00 Kept: 16491
% 27.63/28.00 Inuse: 604
% 27.63/28.00 Deleted: 122
% 27.63/28.00 Deletedinuse: 49
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 106147
% 27.63/28.00 Kept: 18527
% 27.63/28.00 Inuse: 682
% 27.63/28.00 Deleted: 127
% 27.63/28.00 Deletedinuse: 50
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 384427 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying clauses:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 114923
% 27.63/28.00 Kept: 20533
% 27.63/28.00 Inuse: 710
% 27.63/28.00 Deleted: 1543
% 27.63/28.00 Deletedinuse: 50
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 1297440 integers for clauses
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 126203
% 27.63/28.00 Kept: 22577
% 27.63/28.00 Inuse: 749
% 27.63/28.00 Deleted: 1543
% 27.63/28.00 Deletedinuse: 50
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 143693
% 27.63/28.00 Kept: 24611
% 27.63/28.00 Inuse: 807
% 27.63/28.00 Deleted: 1543
% 27.63/28.00 Deletedinuse: 50
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 156902
% 27.63/28.00 Kept: 26622
% 27.63/28.00 Inuse: 857
% 27.63/28.00 Deleted: 1547
% 27.63/28.00 Deletedinuse: 54
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 576640 integers for termspace/termends
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 172768
% 27.63/28.00 Kept: 28673
% 27.63/28.00 Inuse: 891
% 27.63/28.00 Deleted: 1549
% 27.63/28.00 Deletedinuse: 56
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 189141
% 27.63/28.00 Kept: 30721
% 27.63/28.00 Inuse: 932
% 27.63/28.00 Deleted: 1549
% 27.63/28.00 Deletedinuse: 56
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 199932
% 27.63/28.00 Kept: 32806
% 27.63/28.00 Inuse: 960
% 27.63/28.00 Deleted: 1553
% 27.63/28.00 Deletedinuse: 60
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 1946160 integers for clauses
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 210649
% 27.63/28.00 Kept: 34875
% 27.63/28.00 Inuse: 995
% 27.63/28.00 Deleted: 1556
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 227313
% 27.63/28.00 Kept: 37032
% 27.63/28.00 Inuse: 1039
% 27.63/28.00 Deleted: 1556
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 245047
% 27.63/28.00 Kept: 39199
% 27.63/28.00 Inuse: 1089
% 27.63/28.00 Deleted: 1556
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying clauses:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 253519
% 27.63/28.00 Kept: 41585
% 27.63/28.00 Inuse: 1111
% 27.63/28.00 Deleted: 2680
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 864960 integers for termspace/termends
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 265637
% 27.63/28.00 Kept: 43660
% 27.63/28.00 Inuse: 1139
% 27.63/28.00 Deleted: 2680
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 274775
% 27.63/28.00 Kept: 46691
% 27.63/28.00 Inuse: 1162
% 27.63/28.00 Deleted: 2680
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 286005
% 27.63/28.00 Kept: 48710
% 27.63/28.00 Inuse: 1185
% 27.63/28.00 Deleted: 2680
% 27.63/28.00 Deletedinuse: 63
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 304170
% 27.63/28.00 Kept: 50721
% 27.63/28.00 Inuse: 1221
% 27.63/28.00 Deleted: 2685
% 27.63/28.00 Deletedinuse: 68
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 *** allocated 2919240 integers for clauses
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 318505
% 27.63/28.00 Kept: 53393
% 27.63/28.00 Inuse: 1251
% 27.63/28.00 Deleted: 2685
% 27.63/28.00 Deletedinuse: 68
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 341555
% 27.63/28.00 Kept: 55431
% 27.63/28.00 Inuse: 1281
% 27.63/28.00 Deleted: 2687
% 27.63/28.00 Deletedinuse: 68
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 358417
% 27.63/28.00 Kept: 57480
% 27.63/28.00 Inuse: 1302
% 27.63/28.00 Deleted: 2690
% 27.63/28.00 Deletedinuse: 70
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Intermediate Status:
% 27.63/28.00 Generated: 370379
% 27.63/28.00 Kept: 59538
% 27.63/28.00 Inuse: 1329
% 27.63/28.00 Deleted: 2691
% 27.63/28.00 Deletedinuse: 70
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying clauses:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00 Resimplifying inuse:
% 27.63/28.00 Done
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Bliksems!, er is een bewijs:
% 27.63/28.00 % SZS status Theorem
% 27.63/28.00 % SZS output start Refutation
% 27.63/28.00
% 27.63/28.00 (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 27.63/28.00 (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 27.63/28.00 (4) {G0,W8,D2,L3,V2,M3} I { r1( Y ), Y = X, alpha1( X, Y ) }.
% 27.63/28.00 (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 27.63/28.00 (6) {G0,W9,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), Y = skol2( X ) }.
% 27.63/28.00 (7) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 27.63/28.00 (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 27.63/28.00 (9) {G0,W10,D2,L3,V3,M3} I { r2( X, Z ), Z = Y, alpha2( X, Y, Z ) }.
% 27.63/28.00 (10) {G0,W11,D3,L2,V3,M2} I { alpha3( X, Y, skol3( X, Y ), Z ), r3( X, Y, Z
% 27.63/28.00 ) }.
% 27.63/28.00 (11) {G0,W12,D3,L2,V3,M2} I { alpha3( X, Y, skol3( X, Y ), Z ), Z = skol3(
% 27.63/28.00 X, Y ) }.
% 27.63/28.00 (12) {G0,W9,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), ! r3( X, Y, T ) }.
% 27.63/28.00 (13) {G0,W8,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 27.63/28.00 (16) {G0,W12,D3,L2,V3,M2} I { alpha4( X, Y, skol4( X, Y ), Z ), Z = skol4(
% 27.63/28.00 X, Y ) }.
% 27.63/28.00 (17) {G0,W9,D2,L2,V4,M2} I { ! alpha4( X, Y, Z, T ), ! r4( X, Y, T ) }.
% 27.63/28.00 (20) {G0,W5,D3,L1,V2,M1} I { r2( Y, skol16( Z, Y ) ) }.
% 27.63/28.00 (23) {G0,W7,D3,L1,V2,M1} I { r2( skol19( X, Y ), skol5( X, Y ) ) }.
% 27.63/28.00 (29) {G0,W6,D3,L1,V2,M1} I { r4( X, Y, skol20( X, Y ) ) }.
% 27.63/28.00 (30) {G0,W12,D2,L4,V4,M4} I { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y
% 27.63/28.00 }.
% 27.63/28.00 (31) {G0,W3,D3,L1,V1,M1} I { r1( skol13( Y ) ) }.
% 27.63/28.00 (32) {G0,W6,D3,L1,V1,M1} I { r3( X, skol13( X ), skol7( X ) ) }.
% 27.63/28.00 (33) {G0,W4,D3,L1,V1,M1} I { skol7( X ) ==> X }.
% 27.63/28.00 (34) {G0,W3,D3,L1,V1,M1} I { r1( skol14( Z ) ) }.
% 27.63/28.00 (35) {G0,W5,D3,L1,V1,M1} I { skol8( Y ) ==> skol14( Y ) }.
% 27.63/28.00 (36) {G0,W3,D3,L1,V1,M1} I { r1( skol18( Y ) ) }.
% 27.63/28.00 (37) {G1,W6,D3,L1,V1,M1} I;d(35) { r4( X, skol18( X ), skol14( X ) ) }.
% 27.63/28.00 (38) {G0,W7,D3,L2,V2,M2} I { alpha5( X ), r2( skol15( Y ), skol9( Y ) ) }.
% 27.63/28.00 (39) {G0,W6,D3,L2,V1,M2} I { alpha5( X ), skol9( X ) ==> X }.
% 27.63/28.00 (40) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), r1( skol10( Y ) ) }.
% 27.63/28.00 (41) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), skol10( X ) ==> X }.
% 27.63/28.00 (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 27.63/28.00 (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 27.63/28.00 (44) {G0,W22,D2,L7,V8,M7} I { ! Z = X, ! r4( T, Y, Z ), ! r2( U, T ), ! r1
% 27.63/28.00 ( W ), ! r2( W, U ), ! r3( Y, V1, V0 ), ! V0 = X }.
% 27.63/28.00 (45) {G1,W3,D2,L1,V1,M1} Q(3) { ! alpha1( X, X ) }.
% 27.63/28.00 (46) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 27.63/28.00 (50) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 (51) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 27.63/28.00 (52) {G1,W19,D2,L6,V7,M6} F(44) { ! X = Y, ! r4( Z, T, X ), ! r2( U, Z ), !
% 27.63/28.00 r1( W ), ! r2( W, U ), ! r3( T, V0, X ) }.
% 27.63/28.00 (54) {G2,W2,D2,L1,V0,M1} R(0,45) { r1( skol1 ) }.
% 27.63/28.00 (55) {G3,W2,D2,L1,V0,M1} R(50,54) { alpha5( skol1 ) }.
% 27.63/28.00 (59) {G2,W3,D3,L1,V1,M1} R(50,36) { alpha5( skol18( X ) ) }.
% 27.63/28.00 (61) {G1,W5,D2,L2,V1,M2} R(2,1) { ! r1( X ), X = skol1 }.
% 27.63/28.00 (64) {G1,W4,D3,L1,V2,M1} R(2,31) { ! alpha1( X, skol13( Y ) ) }.
% 27.63/28.00 (65) {G1,W4,D3,L1,V2,M1} R(2,34) { ! alpha1( X, skol14( Y ) ) }.
% 27.63/28.00 (66) {G1,W4,D3,L1,V2,M1} R(2,36) { ! alpha1( X, skol18( Y ) ) }.
% 27.63/28.00 (67) {G2,W4,D3,L1,V1,M1} R(64,1) { skol13( X ) ==> skol1 }.
% 27.63/28.00 (68) {G2,W4,D3,L1,V1,M1} R(65,1) { skol14( X ) ==> skol1 }.
% 27.63/28.00 (69) {G2,W4,D3,L1,V1,M1} R(66,1) { skol18( X ) ==> skol1 }.
% 27.63/28.00 (70) {G1,W5,D2,L2,V1,M2} R(3,0) { ! X = skol1, r1( X ) }.
% 27.63/28.00 (74) {G3,W3,D2,L1,V1,M1} R(51,54) { ! r2( X, skol1 ) }.
% 27.63/28.00 (78) {G2,W5,D2,L2,V1,M2} R(70,50) { ! X = skol1, alpha5( X ) }.
% 27.63/28.00 (83) {G2,W4,D3,L1,V1,M1} R(5,46) { r2( X, skol2( X ) ) }.
% 27.63/28.00 (84) {G3,W3,D3,L1,V1,M1} R(83,51) { ! r1( skol2( X ) ) }.
% 27.63/28.00 (85) {G4,W7,D3,L2,V2,M2} P(4,83);r(84) { r2( X, Y ), alpha1( Y, skol2( X )
% 27.63/28.00 ) }.
% 27.63/28.00 (92) {G1,W9,D3,L2,V2,M2} R(6,3) { alpha2( X, skol2( X ), Y ), ! alpha1(
% 27.63/28.00 skol2( X ), Y ) }.
% 27.63/28.00 (99) {G2,W9,D2,L3,V2,M3} R(61,4) { X = skol1, X = Y, alpha1( Y, X ) }.
% 27.63/28.00 (119) {G1,W6,D3,L1,V3,M1} R(20,7) { ! alpha2( X, Y, skol16( Z, X ) ) }.
% 27.63/28.00 (120) {G2,W4,D3,L1,V2,M1} R(20,51) { ! r1( skol16( X, Y ) ) }.
% 27.63/28.00 (130) {G3,W5,D3,L1,V2,M1} R(120,70) { ! skol16( X, Y ) ==> skol1 }.
% 27.63/28.00 (187) {G3,W3,D3,L1,V1,M1} R(40,59) { r1( skol10( X ) ) }.
% 27.63/28.00 (194) {G4,W4,D3,L1,V1,M1} R(187,61) { skol10( X ) ==> skol1 }.
% 27.63/28.00 (243) {G1,W9,D3,L2,V3,M2} R(13,10) { ! X = skol3( Y, Z ), r3( Y, Z, X ) }.
% 27.63/28.00 (249) {G2,W6,D3,L1,V2,M1} R(119,6) { skol16( X, Y ) ==> skol2( Y ) }.
% 27.63/28.00 (300) {G1,W15,D3,L3,V4,M3} P(9,29) { r4( X, Y, Z ), r2( T, skol20( X, Y ) )
% 27.63/28.00 , alpha2( T, Z, skol20( X, Y ) ) }.
% 27.63/28.00 (319) {G3,W4,D2,L1,V1,M1} S(37);d(69);d(68) { r4( X, skol1, skol1 ) }.
% 27.63/28.00 (339) {G3,W4,D2,L1,V1,M1} S(32);d(67);d(33) { r3( X, skol1, X ) }.
% 27.63/28.00 (375) {G4,W5,D2,L1,V2,M1} R(339,12) { ! alpha3( X, skol1, Y, X ) }.
% 27.63/28.00 (386) {G5,W5,D3,L1,V1,M1} R(375,11) { skol3( X, skol1 ) ==> X }.
% 27.63/28.00 (387) {G6,W8,D2,L2,V2,M2} P(386,11) { alpha3( X, skol1, X, Y ), Y = X }.
% 27.63/28.00 (394) {G4,W5,D2,L1,V2,M1} R(17,319) { ! alpha4( X, skol1, Y, skol1 ) }.
% 27.63/28.00 (396) {G1,W7,D3,L1,V3,M1} R(17,29) { ! alpha4( X, Y, Z, skol20( X, Y ) )
% 27.63/28.00 }.
% 27.63/28.00 (397) {G5,W5,D3,L1,V1,M1} R(394,16) { skol4( X, skol1 ) ==> skol1 }.
% 27.63/28.00 (475) {G5,W5,D2,L2,V1,M2} S(41);d(194) { ! alpha5( X ), skol1 = X }.
% 27.63/28.00 (479) {G6,W6,D2,L2,V1,M2} R(475,78) { skol1 = X, ! X = skol1 }.
% 27.63/28.00 (500) {G6,W3,D3,L1,V1,M1} P(475,130);q;d(249) { ! alpha5( skol2( Y ) ) }.
% 27.63/28.00 (504) {G6,W5,D2,L2,V2,M2} P(475,74) { ! r2( Y, X ), ! alpha5( X ) }.
% 27.63/28.00 (506) {G6,W8,D2,L3,V2,M3} P(1,475) { ! alpha5( Y ), X = Y, alpha1( skol1, X
% 27.63/28.00 ) }.
% 27.63/28.00 (507) {G6,W4,D2,L2,V1,M2} P(475,54) { r1( X ), ! alpha5( X ) }.
% 27.63/28.00 (521) {G7,W4,D3,L1,V2,M1} R(23,504) { ! alpha5( skol5( X, Y ) ) }.
% 27.63/28.00 (620) {G7,W6,D3,L2,V1,M2} R(39,507) { skol9( X ) ==> X, r1( X ) }.
% 27.63/28.00 (621) {G7,W6,D4,L1,V1,M1} R(39,500) { skol9( skol2( X ) ) ==> skol2( X )
% 27.63/28.00 }.
% 27.63/28.00 (685) {G3,W10,D3,L3,V3,M3} R(30,20);d(249) { ! r2( T, Z ), Y = T, ! skol2(
% 27.63/28.00 Y ) = Z }.
% 27.63/28.00 (764) {G4,W7,D3,L2,V2,M2} Q(685) { ! r2( X, skol2( Y ) ), Y = X }.
% 27.63/28.00 (834) {G8,W5,D3,L1,V1,M1} R(38,521) { r2( skol15( X ), skol9( X ) ) }.
% 27.63/28.00 (881) {G9,W6,D3,L1,V2,M1} R(834,7) { ! alpha2( skol15( X ), Y, skol9( X ) )
% 27.63/28.00 }.
% 27.63/28.00 (885) {G9,W6,D4,L1,V1,M1} P(621,834) { r2( skol15( skol2( X ) ), skol2( X )
% 27.63/28.00 ) }.
% 27.63/28.00 (886) {G9,W6,D3,L2,V1,M2} P(620,834) { r2( skol15( X ), X ), r1( X ) }.
% 27.63/28.00 (984) {G10,W6,D4,L1,V1,M1} R(881,6) { skol2( skol15( X ) ) ==> skol9( X )
% 27.63/28.00 }.
% 27.63/28.00 (1075) {G10,W7,D3,L2,V2,M2} R(886,51) { r2( skol15( X ), X ), ! r2( Y, X )
% 27.63/28.00 }.
% 27.63/28.00 (1582) {G2,W7,D3,L1,V2,M1} R(396,16) { skol4( X, Y ) ==> skol20( X, Y ) }.
% 27.63/28.00 (1651) {G6,W5,D3,L1,V1,M1} P(1582,397) { skol20( X, skol1 ) ==> skol1 }.
% 27.63/28.00 (2007) {G2,W7,D3,L2,V2,M2} R(92,7) { ! alpha1( skol2( X ), Y ), ! r2( X, Y
% 27.63/28.00 ) }.
% 27.63/28.00 (2301) {G11,W13,D3,L4,V4,M4} R(1075,30) { ! r2( X, Y ), ! Y = Z, ! r2( T, Z
% 27.63/28.00 ), skol15( Y ) = T }.
% 27.63/28.00 (2330) {G12,W7,D3,L2,V2,M2} F(2301);q { ! r2( X, Y ), skol15( Y ) = X }.
% 27.63/28.00 (2357) {G13,W8,D3,L2,V3,M2} R(2330,8) { ! r2( X, Y ), ! alpha2( Z, X,
% 27.63/28.00 skol15( Y ) ) }.
% 27.63/28.00 (2358) {G13,W5,D4,L1,V1,M1} R(2330,83) { skol15( skol2( X ) ) ==> X }.
% 27.63/28.00 (2361) {G13,W6,D3,L2,V1,M2} R(2330,70) { ! r2( skol1, X ), r1( skol15( X )
% 27.63/28.00 ) }.
% 27.63/28.00 (2628) {G7,W12,D2,L4,V3,M4} P(99,479) { X = Y, ! Y = X, X = Z, alpha1( Z, X
% 27.63/28.00 ) }.
% 27.63/28.00 (2639) {G8,W6,D2,L2,V2,M2} F(2628);r(3) { X = Y, ! Y = X }.
% 27.63/28.00 (2676) {G14,W7,D3,L2,V2,M2} P(2639,885);d(2358) { r2( Y, skol2( X ) ), ! Y
% 27.63/28.00 = X }.
% 27.63/28.00 (2694) {G14,W6,D3,L2,V1,M2} P(2358,2361) { ! r2( skol1, skol2( X ) ), r1( X
% 27.63/28.00 ) }.
% 27.63/28.00 (2750) {G15,W5,D4,L1,V1,M1} R(2694,84) { ! r2( skol1, skol2( skol2( X ) ) )
% 27.63/28.00 }.
% 27.63/28.00 (2869) {G16,W6,D4,L1,V1,M1} R(2750,85) { alpha1( skol2( skol2( X ) ), skol2
% 27.63/28.00 ( skol1 ) ) }.
% 27.63/28.00 (3054) {G17,W5,D3,L1,V1,M1} R(2869,2007) { ! r2( skol2( X ), skol2( skol1 )
% 27.63/28.00 ) }.
% 27.63/28.00 (3085) {G18,W5,D3,L1,V1,M1} P(984,3054) { ! r2( skol9( X ), skol2( skol1 )
% 27.63/28.00 ) }.
% 27.63/28.00 (3143) {G19,W6,D3,L2,V1,M2} P(39,3085) { ! r2( X, skol2( skol1 ) ), alpha5
% 27.63/28.00 ( X ) }.
% 27.63/28.00 (3517) {G15,W6,D3,L2,V1,M2} R(2676,61) { r2( X, skol2( skol1 ) ), ! r1( X )
% 27.63/28.00 }.
% 27.63/28.00 (8962) {G7,W7,D2,L2,V2,M2} R(387,12) { X = Y, ! r3( Y, skol1, X ) }.
% 27.63/28.00 (9877) {G15,W8,D3,L2,V2,M2} R(8962,2676) { ! r3( X, skol1, Y ), r2( Y,
% 27.63/28.00 skol2( X ) ) }.
% 27.63/28.00 (21307) {G6,W7,D2,L2,V2,M2} P(386,243) { ! Y = X, r3( X, skol1, Y ) }.
% 27.63/28.00 (21340) {G7,W8,D3,L2,V2,M2} R(21307,764) { r3( X, skol1, Y ), ! r2( X,
% 27.63/28.00 skol2( Y ) ) }.
% 27.63/28.00 (21369) {G7,W6,D2,L2,V1,M2} R(21307,61) { r3( skol1, skol1, X ), ! r1( X )
% 27.63/28.00 }.
% 27.63/28.00 (21555) {G8,W6,D2,L2,V1,M2} R(21369,507) { r3( skol1, skol1, X ), ! alpha5
% 27.63/28.00 ( X ) }.
% 27.63/28.00 (21730) {G9,W8,D2,L3,V2,M3} P(506,21555);r(45) { r3( X, X, Y ), ! alpha5( Y
% 27.63/28.00 ), ! alpha5( X ) }.
% 27.63/28.00 (23261) {G10,W6,D2,L2,V1,M2} R(21730,55) { r3( X, X, skol1 ), ! alpha5( X )
% 27.63/28.00 }.
% 27.63/28.00 (23310) {G20,W8,D3,L2,V1,M2} R(23261,3143) { r3( X, X, skol1 ), ! r2( X,
% 27.63/28.00 skol2( skol1 ) ) }.
% 27.63/28.00 (31527) {G16,W8,D2,L2,V3,M2} R(9877,2357);d(2358) { ! r3( X, skol1, Y ), !
% 27.63/28.00 alpha2( Z, Y, X ) }.
% 27.63/28.00 (31937) {G17,W8,D3,L2,V3,M2} R(31527,21340) { ! alpha2( X, Y, Z ), ! r2( Z
% 27.63/28.00 , skol2( Y ) ) }.
% 27.63/28.00 (34214) {G7,W8,D2,L2,V3,M2} P(1651,300);r(74) { r4( X, skol1, Y ), alpha2(
% 27.63/28.00 Z, Y, skol1 ) }.
% 27.63/28.00 (34222) {G18,W8,D3,L2,V2,M2} R(34214,31937) { r4( X, skol1, Y ), ! r2(
% 27.63/28.00 skol1, skol2( Y ) ) }.
% 27.63/28.00 (36406) {G19,W12,D3,L3,V3,M3} P(764,34222) { r4( Y, X, Z ), ! r2( X, skol2
% 27.63/28.00 ( Z ) ), ! r2( X, skol2( skol1 ) ) }.
% 27.63/28.00 (60876) {G21,W15,D3,L5,V5,M5} R(23310,52);r(36406) { ! r2( X, skol2( skol1
% 27.63/28.00 ) ), ! skol1 = Y, ! r2( T, Z ), ! r1( U ), ! r2( U, T ) }.
% 27.63/28.00 (60958) {G22,W12,D3,L4,V4,M4} Q(60876) { ! r2( X, skol2( skol1 ) ), ! r2( Y
% 27.63/28.00 , Z ), ! r1( T ), ! r2( T, Y ) }.
% 27.63/28.00 (60959) {G23,W6,D3,L2,V2,M2} F(60958);r(3517) { ! r2( skol2( skol1 ), Y ),
% 27.63/28.00 ! r1( X ) }.
% 27.63/28.00 (61070) {G24,W2,D2,L1,V1,M1} R(60959,83) { ! r1( X ) }.
% 27.63/28.00 (61135) {G25,W0,D0,L0,V0,M0} R(61070,54) { }.
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 % SZS output end Refutation
% 27.63/28.00 found a proof!
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Unprocessed initial clauses:
% 27.63/28.00
% 27.63/28.00 (61137) {G0,W5,D2,L2,V1,M2} { alpha1( skol1, X ), r1( X ) }.
% 27.63/28.00 (61138) {G0,W6,D2,L2,V1,M2} { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 (61139) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 (61140) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = X }.
% 27.63/28.00 (61141) {G0,W8,D2,L3,V2,M3} { r1( Y ), Y = X, alpha1( X, Y ) }.
% 27.63/28.00 (61142) {G0,W8,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), r2( X, Y ) }.
% 27.63/28.00 (61143) {G0,W9,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), Y = skol2( X )
% 27.63/28.00 }.
% 27.63/28.00 (61144) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! r2( X, Z ) }.
% 27.63/28.00 (61145) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! Z = Y }.
% 27.63/28.00 (61146) {G0,W10,D2,L3,V3,M3} { r2( X, Z ), Z = Y, alpha2( X, Y, Z ) }.
% 27.63/28.00 (61147) {G0,W11,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ), r3( X, Y
% 27.63/28.00 , Z ) }.
% 27.63/28.00 (61148) {G0,W12,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ), Z = skol3
% 27.63/28.00 ( X, Y ) }.
% 27.63/28.00 (61149) {G0,W9,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! r3( X, Y, T ) }.
% 27.63/28.00 (61150) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 27.63/28.00 (61151) {G0,W12,D2,L3,V4,M3} { r3( X, Y, T ), T = Z, alpha3( X, Y, Z, T )
% 27.63/28.00 }.
% 27.63/28.00 (61152) {G0,W11,D3,L2,V3,M2} { alpha4( X, Y, skol4( X, Y ), Z ), r4( X, Y
% 27.63/28.00 , Z ) }.
% 27.63/28.00 (61153) {G0,W12,D3,L2,V3,M2} { alpha4( X, Y, skol4( X, Y ), Z ), Z = skol4
% 27.63/28.00 ( X, Y ) }.
% 27.63/28.00 (61154) {G0,W9,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), ! r4( X, Y, T ) }.
% 27.63/28.00 (61155) {G0,W8,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), ! T = Z }.
% 27.63/28.00 (61156) {G0,W12,D2,L3,V4,M3} { r4( X, Y, T ), T = Z, alpha4( X, Y, Z, T )
% 27.63/28.00 }.
% 27.63/28.00 (61157) {G0,W5,D3,L1,V2,M1} { r2( Y, skol16( Z, Y ) ) }.
% 27.63/28.00 (61158) {G0,W8,D3,L1,V2,M1} { r3( X, skol16( X, Y ), skol11( X, Y ) ) }.
% 27.63/28.00 (61159) {G0,W7,D3,L1,V2,M1} { skol11( X, Y ) = skol5( X, Y ) }.
% 27.63/28.00 (61160) {G0,W7,D3,L1,V2,M1} { r2( skol19( X, Y ), skol5( X, Y ) ) }.
% 27.63/28.00 (61161) {G0,W6,D3,L1,V2,M1} { r3( X, Y, skol19( X, Y ) ) }.
% 27.63/28.00 (61162) {G0,W5,D3,L1,V2,M1} { r2( Y, skol17( Z, Y ) ) }.
% 27.63/28.00 (61163) {G0,W8,D3,L1,V2,M1} { r4( X, skol17( X, Y ), skol12( X, Y ) ) }.
% 27.63/28.00 (61164) {G0,W7,D3,L1,V2,M1} { skol12( X, Y ) = skol6( X, Y ) }.
% 27.63/28.00 (61165) {G0,W8,D3,L1,V2,M1} { r3( skol20( X, Y ), X, skol6( X, Y ) ) }.
% 27.63/28.00 (61166) {G0,W6,D3,L1,V2,M1} { r4( X, Y, skol20( X, Y ) ) }.
% 27.63/28.00 (61167) {G0,W12,D2,L4,V4,M4} { ! r2( X, T ), ! T = Z, ! r2( Y, Z ), X = Y
% 27.63/28.00 }.
% 27.63/28.00 (61168) {G0,W3,D3,L1,V1,M1} { r1( skol13( Y ) ) }.
% 27.63/28.00 (61169) {G0,W6,D3,L1,V1,M1} { r3( X, skol13( X ), skol7( X ) ) }.
% 27.63/28.00 (61170) {G0,W4,D3,L1,V1,M1} { skol7( X ) = X }.
% 27.63/28.00 (61171) {G0,W3,D3,L1,V1,M1} { r1( skol14( Z ) ) }.
% 27.63/28.00 (61172) {G0,W5,D3,L1,V1,M1} { skol8( Y ) = skol14( Y ) }.
% 27.63/28.00 (61173) {G0,W3,D3,L1,V1,M1} { r1( skol18( Y ) ) }.
% 27.63/28.00 (61174) {G0,W6,D3,L1,V1,M1} { r4( X, skol18( X ), skol8( X ) ) }.
% 27.63/28.00 (61175) {G0,W7,D3,L2,V2,M2} { alpha5( X ), r2( skol15( Y ), skol9( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 (61176) {G0,W6,D3,L2,V1,M2} { alpha5( X ), X = skol9( X ) }.
% 27.63/28.00 (61177) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), r1( skol10( Y ) ) }.
% 27.63/28.00 (61178) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), X = skol10( X ) }.
% 27.63/28.00 (61179) {G0,W7,D2,L3,V2,M3} { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 27.63/28.00 (61180) {G0,W8,D2,L3,V3,M3} { ! r1( Y ), ! Y = X, ! r2( Z, X ) }.
% 27.63/28.00 (61181) {G0,W22,D2,L7,V8,M7} { ! Z = X, ! r4( T, Y, Z ), ! r2( U, T ), !
% 27.63/28.00 r1( W ), ! r2( W, U ), ! r3( Y, V1, V0 ), ! V0 = X }.
% 27.63/28.00
% 27.63/28.00
% 27.63/28.00 Total Proof:
% 27.63/28.00
% 27.63/28.00 subsumption: (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 27.63/28.00 parent0: (61137) {G0,W5,D2,L2,V1,M2} { alpha1( skol1, X ), r1( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 parent0: (61138) {G0,W6,D2,L2,V1,M2} { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 parent0: (61139) {G0,W5,D2,L2,V2,M2} { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 27.63/28.00 parent0: (61140) {G0,W6,D2,L2,V2,M2} { ! alpha1( X, Y ), ! Y = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (4) {G0,W8,D2,L3,V2,M3} I { r1( Y ), Y = X, alpha1( X, Y ) }.
% 27.63/28.00 parent0: (61141) {G0,W8,D2,L3,V2,M3} { r1( Y ), Y = X, alpha1( X, Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X
% 27.63/28.00 , Y ) }.
% 27.63/28.00 parent0: (61142) {G0,W8,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), r2( X,
% 27.63/28.00 Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (6) {G0,W9,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), Y =
% 27.63/28.00 skol2( X ) }.
% 27.63/28.00 parent0: (61143) {G0,W9,D3,L2,V2,M2} { alpha2( X, skol2( X ), Y ), Y =
% 27.63/28.00 skol2( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (7) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! r2( X, Z )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61144) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! r2( X, Z )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 27.63/28.00 parent0: (61145) {G0,W7,D2,L2,V3,M2} { ! alpha2( X, Y, Z ), ! Z = Y }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (9) {G0,W10,D2,L3,V3,M3} I { r2( X, Z ), Z = Y, alpha2( X, Y,
% 27.63/28.00 Z ) }.
% 27.63/28.00 parent0: (61146) {G0,W10,D2,L3,V3,M3} { r2( X, Z ), Z = Y, alpha2( X, Y, Z
% 27.63/28.00 ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (10) {G0,W11,D3,L2,V3,M2} I { alpha3( X, Y, skol3( X, Y ), Z )
% 27.63/28.00 , r3( X, Y, Z ) }.
% 27.63/28.00 parent0: (61147) {G0,W11,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ),
% 27.63/28.00 r3( X, Y, Z ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (11) {G0,W12,D3,L2,V3,M2} I { alpha3( X, Y, skol3( X, Y ), Z )
% 27.63/28.00 , Z = skol3( X, Y ) }.
% 27.63/28.00 parent0: (61148) {G0,W12,D3,L2,V3,M2} { alpha3( X, Y, skol3( X, Y ), Z ),
% 27.63/28.00 Z = skol3( X, Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (12) {G0,W9,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), ! r3( X,
% 27.63/28.00 Y, T ) }.
% 27.63/28.00 parent0: (61149) {G0,W9,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! r3( X, Y
% 27.63/28.00 , T ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (13) {G0,W8,D2,L2,V4,M2} I { ! alpha3( X, Y, Z, T ), ! T = Z
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61150) {G0,W8,D2,L2,V4,M2} { ! alpha3( X, Y, Z, T ), ! T = Z }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (16) {G0,W12,D3,L2,V3,M2} I { alpha4( X, Y, skol4( X, Y ), Z )
% 27.63/28.00 , Z = skol4( X, Y ) }.
% 27.63/28.00 parent0: (61153) {G0,W12,D3,L2,V3,M2} { alpha4( X, Y, skol4( X, Y ), Z ),
% 27.63/28.00 Z = skol4( X, Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (17) {G0,W9,D2,L2,V4,M2} I { ! alpha4( X, Y, Z, T ), ! r4( X,
% 27.63/28.00 Y, T ) }.
% 27.63/28.00 parent0: (61154) {G0,W9,D2,L2,V4,M2} { ! alpha4( X, Y, Z, T ), ! r4( X, Y
% 27.63/28.00 , T ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (20) {G0,W5,D3,L1,V2,M1} I { r2( Y, skol16( Z, Y ) ) }.
% 27.63/28.00 parent0: (61157) {G0,W5,D3,L1,V2,M1} { r2( Y, skol16( Z, Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := T
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (23) {G0,W7,D3,L1,V2,M1} I { r2( skol19( X, Y ), skol5( X, Y )
% 27.63/28.00 ) }.
% 27.63/28.00 parent0: (61160) {G0,W7,D3,L1,V2,M1} { r2( skol19( X, Y ), skol5( X, Y ) )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (29) {G0,W6,D3,L1,V2,M1} I { r4( X, Y, skol20( X, Y ) ) }.
% 27.63/28.00 parent0: (61166) {G0,W6,D3,L1,V2,M1} { r4( X, Y, skol20( X, Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (30) {G0,W12,D2,L4,V4,M4} I { ! r2( X, T ), ! T = Z, ! r2( Y,
% 27.63/28.00 Z ), X = Y }.
% 27.63/28.00 parent0: (61167) {G0,W12,D2,L4,V4,M4} { ! r2( X, T ), ! T = Z, ! r2( Y, Z
% 27.63/28.00 ), X = Y }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 3 ==> 3
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (31) {G0,W3,D3,L1,V1,M1} I { r1( skol13( Y ) ) }.
% 27.63/28.00 parent0: (61168) {G0,W3,D3,L1,V1,M1} { r1( skol13( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (32) {G0,W6,D3,L1,V1,M1} I { r3( X, skol13( X ), skol7( X ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61169) {G0,W6,D3,L1,V1,M1} { r3( X, skol13( X ), skol7( X ) )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (33) {G0,W4,D3,L1,V1,M1} I { skol7( X ) ==> X }.
% 27.63/28.00 parent0: (61170) {G0,W4,D3,L1,V1,M1} { skol7( X ) = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (34) {G0,W3,D3,L1,V1,M1} I { r1( skol14( Z ) ) }.
% 27.63/28.00 parent0: (61171) {G0,W3,D3,L1,V1,M1} { r1( skol14( Z ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := T
% 27.63/28.00 Y := U
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (35) {G0,W5,D3,L1,V1,M1} I { skol8( Y ) ==> skol14( Y ) }.
% 27.63/28.00 parent0: (61172) {G0,W5,D3,L1,V1,M1} { skol8( Y ) = skol14( Y ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (36) {G0,W3,D3,L1,V1,M1} I { r1( skol18( Y ) ) }.
% 27.63/28.00 parent0: (61173) {G0,W3,D3,L1,V1,M1} { r1( skol18( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 paramod: (61474) {G1,W6,D3,L1,V1,M1} { r4( X, skol18( X ), skol14( X ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0[0]: (35) {G0,W5,D3,L1,V1,M1} I { skol8( Y ) ==> skol14( Y ) }.
% 27.63/28.00 parent1[0; 4]: (61174) {G0,W6,D3,L1,V1,M1} { r4( X, skol18( X ), skol8( X
% 27.63/28.00 ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (37) {G1,W6,D3,L1,V1,M1} I;d(35) { r4( X, skol18( X ), skol14
% 27.63/28.00 ( X ) ) }.
% 27.63/28.00 parent0: (61474) {G1,W6,D3,L1,V1,M1} { r4( X, skol18( X ), skol14( X ) )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (38) {G0,W7,D3,L2,V2,M2} I { alpha5( X ), r2( skol15( Y ),
% 27.63/28.00 skol9( Y ) ) }.
% 27.63/28.00 parent0: (61175) {G0,W7,D3,L2,V2,M2} { alpha5( X ), r2( skol15( Y ), skol9
% 27.63/28.00 ( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61511) {G0,W6,D3,L2,V1,M2} { skol9( X ) = X, alpha5( X ) }.
% 27.63/28.00 parent0[1]: (61176) {G0,W6,D3,L2,V1,M2} { alpha5( X ), X = skol9( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (39) {G0,W6,D3,L2,V1,M2} I { alpha5( X ), skol9( X ) ==> X }.
% 27.63/28.00 parent0: (61511) {G0,W6,D3,L2,V1,M2} { skol9( X ) = X, alpha5( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 1
% 27.63/28.00 1 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (40) {G0,W5,D3,L2,V2,M2} I { ! alpha5( X ), r1( skol10( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61177) {G0,W5,D3,L2,V2,M2} { ! alpha5( X ), r1( skol10( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61550) {G0,W6,D3,L2,V1,M2} { skol10( X ) = X, ! alpha5( X ) }.
% 27.63/28.00 parent0[1]: (61178) {G0,W6,D3,L2,V1,M2} { ! alpha5( X ), X = skol10( X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (41) {G0,W6,D3,L2,V1,M2} I { ! alpha5( X ), skol10( X ) ==> X
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61550) {G0,W6,D3,L2,V1,M2} { skol10( X ) = X, ! alpha5( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 1
% 27.63/28.00 1 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61179) {G0,W7,D2,L3,V2,M3} { ! r1( Y ), ! X = Y, alpha5( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61180) {G0,W8,D2,L3,V3,M3} { ! r1( Y ), ! Y = X, ! r2( Z, X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (44) {G0,W22,D2,L7,V8,M7} I { ! Z = X, ! r4( T, Y, Z ), ! r2(
% 27.63/28.00 U, T ), ! r1( W ), ! r2( W, U ), ! r3( Y, V1, V0 ), ! V0 = X }.
% 27.63/28.00 parent0: (61181) {G0,W22,D2,L7,V8,M7} { ! Z = X, ! r4( T, Y, Z ), ! r2( U
% 27.63/28.00 , T ), ! r1( W ), ! r2( W, U ), ! r3( Y, V1, V0 ), ! V0 = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 U := U
% 27.63/28.00 W := W
% 27.63/28.00 V0 := V0
% 27.63/28.00 V1 := V1
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 3 ==> 3
% 27.63/28.00 4 ==> 4
% 27.63/28.00 5 ==> 5
% 27.63/28.00 6 ==> 6
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61627) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 27.63/28.00 parent0[1]: (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqrefl: (61628) {G0,W3,D2,L1,V1,M1} { ! alpha1( X, X ) }.
% 27.63/28.00 parent0[0]: (61627) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (45) {G1,W3,D2,L1,V1,M1} Q(3) { ! alpha1( X, X ) }.
% 27.63/28.00 parent0: (61628) {G0,W3,D2,L1,V1,M1} { ! alpha1( X, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61629) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha2( Z, Y, X ) }.
% 27.63/28.00 parent0[1]: (8) {G0,W7,D2,L2,V3,M2} I { ! alpha2( X, Y, Z ), ! Z = Y }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqrefl: (61630) {G0,W4,D2,L1,V2,M1} { ! alpha2( Y, X, X ) }.
% 27.63/28.00 parent0[0]: (61629) {G0,W7,D2,L2,V3,M2} { ! Y = X, ! alpha2( Z, Y, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := X
% 27.63/28.00 Z := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (46) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 27.63/28.00 parent0: (61630) {G0,W4,D2,L1,V2,M1} { ! alpha2( Y, X, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61631) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! r1( Y ), alpha5( X ) }.
% 27.63/28.00 parent0[1]: (42) {G0,W7,D2,L3,V2,M3} I { ! r1( Y ), ! X = Y, alpha5( X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqrefl: (61632) {G0,W4,D2,L2,V1,M2} { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 parent0[0]: (61631) {G0,W7,D2,L3,V2,M3} { ! Y = X, ! r1( Y ), alpha5( X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (50) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 parent0: (61632) {G0,W4,D2,L2,V1,M2} { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61633) {G0,W8,D2,L3,V3,M3} { ! Y = X, ! r1( X ), ! r2( Z, Y ) }.
% 27.63/28.00 parent0[1]: (43) {G0,W8,D2,L3,V3,M3} I { ! r1( Y ), ! Y = X, ! r2( Z, X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := X
% 27.63/28.00 Z := Z
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqrefl: (61634) {G0,W5,D2,L2,V2,M2} { ! r1( X ), ! r2( Y, X ) }.
% 27.63/28.00 parent0[0]: (61633) {G0,W8,D2,L3,V3,M3} { ! Y = X, ! r1( X ), ! r2( Z, Y )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := X
% 27.63/28.00 Z := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (51) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 27.63/28.00 parent0: (61634) {G0,W5,D2,L2,V2,M2} { ! r1( X ), ! r2( Y, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 factor: (61638) {G0,W19,D2,L6,V7,M6} { ! X = Y, ! r4( Z, T, X ), ! r2( U,
% 27.63/28.00 Z ), ! r1( W ), ! r2( W, U ), ! r3( T, V0, X ) }.
% 27.63/28.00 parent0[0, 6]: (44) {G0,W22,D2,L7,V8,M7} I { ! Z = X, ! r4( T, Y, Z ), ! r2
% 27.63/28.00 ( U, T ), ! r1( W ), ! r2( W, U ), ! r3( Y, V1, V0 ), ! V0 = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := T
% 27.63/28.00 Z := X
% 27.63/28.00 T := Z
% 27.63/28.00 U := U
% 27.63/28.00 W := W
% 27.63/28.00 V0 := X
% 27.63/28.00 V1 := V0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (52) {G1,W19,D2,L6,V7,M6} F(44) { ! X = Y, ! r4( Z, T, X ), !
% 27.63/28.00 r2( U, Z ), ! r1( W ), ! r2( W, U ), ! r3( T, V0, X ) }.
% 27.63/28.00 parent0: (61638) {G0,W19,D2,L6,V7,M6} { ! X = Y, ! r4( Z, T, X ), ! r2( U
% 27.63/28.00 , Z ), ! r1( W ), ! r2( W, U ), ! r3( T, V0, X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 Z := Z
% 27.63/28.00 T := T
% 27.63/28.00 U := U
% 27.63/28.00 W := W
% 27.63/28.00 V0 := V0
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 1 ==> 1
% 27.63/28.00 2 ==> 2
% 27.63/28.00 3 ==> 3
% 27.63/28.00 4 ==> 4
% 27.63/28.00 5 ==> 5
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61646) {G1,W2,D2,L1,V0,M1} { r1( skol1 ) }.
% 27.63/28.00 parent0[0]: (45) {G1,W3,D2,L1,V1,M1} Q(3) { ! alpha1( X, X ) }.
% 27.63/28.00 parent1[0]: (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol1
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := skol1
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (54) {G2,W2,D2,L1,V0,M1} R(0,45) { r1( skol1 ) }.
% 27.63/28.00 parent0: (61646) {G1,W2,D2,L1,V0,M1} { r1( skol1 ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61647) {G2,W2,D2,L1,V0,M1} { alpha5( skol1 ) }.
% 27.63/28.00 parent0[0]: (50) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 parent1[0]: (54) {G2,W2,D2,L1,V0,M1} R(0,45) { r1( skol1 ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol1
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (55) {G3,W2,D2,L1,V0,M1} R(50,54) { alpha5( skol1 ) }.
% 27.63/28.00 parent0: (61647) {G2,W2,D2,L1,V0,M1} { alpha5( skol1 ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61648) {G1,W3,D3,L1,V1,M1} { alpha5( skol18( X ) ) }.
% 27.63/28.00 parent0[0]: (50) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 27.63/28.00 parent1[0]: (36) {G0,W3,D3,L1,V1,M1} I { r1( skol18( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol18( X )
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := Y
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (59) {G2,W3,D3,L1,V1,M1} R(50,36) { alpha5( skol18( X ) ) }.
% 27.63/28.00 parent0: (61648) {G1,W3,D3,L1,V1,M1} { alpha5( skol18( X ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61649) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 27.63/28.00 parent0[1]: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61650) {G1,W5,D2,L2,V1,M2} { ! r1( X ), skol1 = X }.
% 27.63/28.00 parent0[0]: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 parent1[1]: (61649) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol1
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61651) {G1,W5,D2,L2,V1,M2} { X = skol1, ! r1( X ) }.
% 27.63/28.00 parent0[1]: (61650) {G1,W5,D2,L2,V1,M2} { ! r1( X ), skol1 = X }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (61) {G1,W5,D2,L2,V1,M2} R(2,1) { ! r1( X ), X = skol1 }.
% 27.63/28.00 parent0: (61651) {G1,W5,D2,L2,V1,M2} { X = skol1, ! r1( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 1
% 27.63/28.00 1 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61652) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol13( Y ) ) }.
% 27.63/28.00 parent0[1]: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 parent1[0]: (31) {G0,W3,D3,L1,V1,M1} I { r1( skol13( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := skol13( Y )
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (64) {G1,W4,D3,L1,V2,M1} R(2,31) { ! alpha1( X, skol13( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61652) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol13( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61653) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol14( Y ) ) }.
% 27.63/28.00 parent0[1]: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 parent1[0]: (34) {G0,W3,D3,L1,V1,M1} I { r1( skol14( Z ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := skol14( Y )
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := T
% 27.63/28.00 Z := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (65) {G1,W4,D3,L1,V2,M1} R(2,34) { ! alpha1( X, skol14( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61653) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol14( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61654) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol18( Y ) ) }.
% 27.63/28.00 parent0[1]: (2) {G0,W5,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! r1( Y ) }.
% 27.63/28.00 parent1[0]: (36) {G0,W3,D3,L1,V1,M1} I { r1( skol18( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := skol18( Y )
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := Z
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (66) {G1,W4,D3,L1,V2,M1} R(2,36) { ! alpha1( X, skol18( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent0: (61654) {G1,W4,D3,L1,V2,M1} { ! alpha1( X, skol18( Y ) ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 Y := Y
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61655) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 27.63/28.00 parent0[1]: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61656) {G1,W4,D3,L1,V1,M1} { skol1 = skol13( X ) }.
% 27.63/28.00 parent0[0]: (64) {G1,W4,D3,L1,V2,M1} R(2,31) { ! alpha1( X, skol13( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent1[1]: (61655) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol1
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := skol13( X )
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61657) {G1,W4,D3,L1,V1,M1} { skol13( X ) = skol1 }.
% 27.63/28.00 parent0[0]: (61656) {G1,W4,D3,L1,V1,M1} { skol1 = skol13( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (67) {G2,W4,D3,L1,V1,M1} R(64,1) { skol13( X ) ==> skol1 }.
% 27.63/28.00 parent0: (61657) {G1,W4,D3,L1,V1,M1} { skol13( X ) = skol1 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00 permutation0:
% 27.63/28.00 0 ==> 0
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61658) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 27.63/28.00 parent0[1]: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 resolution: (61659) {G1,W4,D3,L1,V1,M1} { skol1 = skol14( X ) }.
% 27.63/28.00 parent0[0]: (65) {G1,W4,D3,L1,V2,M1} R(2,34) { ! alpha1( X, skol14( Y ) )
% 27.63/28.00 }.
% 27.63/28.00 parent1[1]: (61658) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X )
% 27.63/28.00 }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := skol1
% 27.63/28.00 Y := X
% 27.63/28.00 end
% 27.63/28.00 substitution1:
% 27.63/28.00 X := skol14( X )
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 eqswap: (61660) {G1,W4,D3,L1,V1,M1} { skol14( X ) = skol1 }.
% 27.63/28.00 parent0[0]: (61659) {G1,W4,D3,L1,V1,M1} { skol1 = skol14( X ) }.
% 27.63/28.00 substitution0:
% 27.63/28.00 X := X
% 27.63/28.00 end
% 27.63/28.00
% 27.63/28.00 subsumption: (68) {G2,W4,D3,L1,V1,M1} R(65,1) { skol14( X ) ==> skol1 }.
% 27.63/28.00 parent0: (61660) {G1,W4,D3,L1,V1,M1} { skol14( X ) = skol1 }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61661) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X ) }.
% 27.83/28.24 parent0[1]: (1) {G0,W6,D2,L2,V1,M2} I { alpha1( skol1, X ), X = skol1 }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61662) {G1,W4,D3,L1,V1,M1} { skol1 = skol18( X ) }.
% 27.83/28.24 parent0[0]: (66) {G1,W4,D3,L1,V2,M1} R(2,36) { ! alpha1( X, skol18( Y ) )
% 27.83/28.24 }.
% 27.83/28.24 parent1[1]: (61661) {G0,W6,D2,L2,V1,M2} { skol1 = X, alpha1( skol1, X )
% 27.83/28.24 }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := skol1
% 27.83/28.24 Y := X
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 X := skol18( X )
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61663) {G1,W4,D3,L1,V1,M1} { skol18( X ) = skol1 }.
% 27.83/28.24 parent0[0]: (61662) {G1,W4,D3,L1,V1,M1} { skol1 = skol18( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (69) {G2,W4,D3,L1,V1,M1} R(66,1) { skol18( X ) ==> skol1 }.
% 27.83/28.24 parent0: (61663) {G1,W4,D3,L1,V1,M1} { skol18( X ) = skol1 }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61664) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 27.83/28.24 parent0[1]: (3) {G0,W6,D2,L2,V2,M2} I { ! alpha1( X, Y ), ! Y = X }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := Y
% 27.83/28.24 Y := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61665) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 27.83/28.24 parent0[1]: (61664) {G0,W6,D2,L2,V2,M2} { ! Y = X, ! alpha1( Y, X ) }.
% 27.83/28.24 parent1[0]: (0) {G0,W5,D2,L2,V1,M2} I { alpha1( skol1, X ), r1( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 Y := skol1
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61666) {G1,W5,D2,L2,V1,M2} { ! X = skol1, r1( X ) }.
% 27.83/28.24 parent0[0]: (61665) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (70) {G1,W5,D2,L2,V1,M2} R(3,0) { ! X = skol1, r1( X ) }.
% 27.83/28.24 parent0: (61666) {G1,W5,D2,L2,V1,M2} { ! X = skol1, r1( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 1 ==> 1
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61667) {G2,W3,D2,L1,V1,M1} { ! r2( X, skol1 ) }.
% 27.83/28.24 parent0[0]: (51) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 27.83/28.24 parent1[0]: (54) {G2,W2,D2,L1,V0,M1} R(0,45) { r1( skol1 ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := skol1
% 27.83/28.24 Y := X
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (74) {G3,W3,D2,L1,V1,M1} R(51,54) { ! r2( X, skol1 ) }.
% 27.83/28.24 parent0: (61667) {G2,W3,D2,L1,V1,M1} { ! r2( X, skol1 ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61668) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 27.83/28.24 parent0[0]: (70) {G1,W5,D2,L2,V1,M2} R(3,0) { ! X = skol1, r1( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61669) {G2,W5,D2,L2,V1,M2} { alpha5( X ), ! skol1 = X }.
% 27.83/28.24 parent0[0]: (50) {G1,W4,D2,L2,V1,M2} Q(42) { ! r1( X ), alpha5( X ) }.
% 27.83/28.24 parent1[1]: (61668) {G1,W5,D2,L2,V1,M2} { ! skol1 = X, r1( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 eqswap: (61670) {G2,W5,D2,L2,V1,M2} { ! X = skol1, alpha5( X ) }.
% 27.83/28.24 parent0[1]: (61669) {G2,W5,D2,L2,V1,M2} { alpha5( X ), ! skol1 = X }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (78) {G2,W5,D2,L2,V1,M2} R(70,50) { ! X = skol1, alpha5( X )
% 27.83/28.24 }.
% 27.83/28.24 parent0: (61670) {G2,W5,D2,L2,V1,M2} { ! X = skol1, alpha5( X ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 1 ==> 1
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61671) {G1,W4,D3,L1,V1,M1} { r2( X, skol2( X ) ) }.
% 27.83/28.24 parent0[0]: (46) {G1,W4,D2,L1,V2,M1} Q(8) { ! alpha2( X, Y, Y ) }.
% 27.83/28.24 parent1[0]: (5) {G0,W8,D3,L2,V2,M2} I { alpha2( X, skol2( X ), Y ), r2( X,
% 27.83/28.24 Y ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 Y := skol2( X )
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 X := X
% 27.83/28.24 Y := skol2( X )
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (83) {G2,W4,D3,L1,V1,M1} R(5,46) { r2( X, skol2( X ) ) }.
% 27.83/28.24 parent0: (61671) {G1,W4,D3,L1,V1,M1} { r2( X, skol2( X ) ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 resolution: (61672) {G2,W3,D3,L1,V1,M1} { ! r1( skol2( X ) ) }.
% 27.83/28.24 parent0[1]: (51) {G1,W5,D2,L2,V2,M2} Q(43) { ! r1( X ), ! r2( Y, X ) }.
% 27.83/28.24 parent1[0]: (83) {G2,W4,D3,L1,V1,M1} R(5,46) { r2( X, skol2( X ) ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := skol2( X )
% 27.83/28.24 Y := X
% 27.83/28.24 end
% 27.83/28.24 substitution1:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 subsumption: (84) {G3,W3,D3,L1,V1,M1} R(83,51) { ! r1( skol2( X ) ) }.
% 27.83/28.24 parent0: (61672) {G2,W3,D3,L1,V1,M1} { ! r1( skol2( X ) ) }.
% 27.83/28.24 substitution0:
% 27.83/28.24 X := X
% 27.83/28.24 end
% 27.83/28.24 permutation0:
% 27.83/28.24 0 ==> 0
% 27.83/28.24 end
% 27.83/28.24
% 27.83/28.24 *** allocated 15000 integers for justifications
% 27.83/28.24 *** allocated 22500 integers forCputime limit exceeded (core dumped)
%------------------------------------------------------------------------------