%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM466+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n029.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Mon Jul 18 06:22:33 EDT 2022
% Result : Theorem 48.24s 48.61s
% Output : Refutation 48.24s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13 % Problem : NUM466+2 : TPTP v8.1.0. Released v4.0.0.
% 0.08/0.13 % Command : bliksem %s
% 0.14/0.35 % Computer : n029.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % DateTime : Wed Jul 6 07:56:43 EDT 2022
% 0.14/0.35 % CPUTime :
% 0.78/1.12 *** allocated 10000 integers for termspace/termends
% 0.78/1.12 *** allocated 10000 integers for clauses
% 0.78/1.12 *** allocated 10000 integers for justifications
% 0.78/1.12 Bliksem 1.12
% 0.78/1.12
% 0.78/1.12
% 0.78/1.12 Automatic Strategy Selection
% 0.78/1.12
% 0.78/1.12
% 0.78/1.12 Clauses:
% 0.78/1.12
% 0.78/1.12 { && }.
% 0.78/1.12 { aNaturalNumber0( sz00 ) }.
% 0.78/1.12 { aNaturalNumber0( sz10 ) }.
% 0.78/1.12 { ! sz10 = sz00 }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.78/1.12 ( X, Y ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.78/1.12 ( X, Y ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.78/1.12 sdtpldt0( Y, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.78/1.12 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.78/1.12 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.78/1.12 sdtasdt0( Y, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.78/1.12 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.78/1.12 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.78/1.12 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.78/1.12 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.78/1.12 , Z ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.78/1.12 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.78/1.12 , X ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.78/1.12 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.78/1.12 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.78/1.12 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.78/1.12 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.78/1.12 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.78/1.12 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.78/1.12 , X = sz00 }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.78/1.12 , Y = sz00 }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.78/1.12 , X = sz00, Y = sz00 }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.78/1.12 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.78/1.12 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.78/1.12 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.78/1.12 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.78/1.12 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.78/1.12 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.78/1.12 sdtlseqdt0( Y, X ), X = Y }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.78/1.12 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.78/1.12 X }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.78/1.12 sdtlseqdt0( Y, X ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.78/1.12 ), ! aNaturalNumber0( Z ), alpha1( X, Y, Z ) }.
% 0.78/1.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.78/1.12 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.78/1.12 ) ) }.
% 0.78/1.12 { ! alpha1( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.78/1.12 { ! alpha1( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.78/1.12 { ! alpha1( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 17.73/18.12 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 17.73/18.12 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha1( X, Y, Z
% 17.73/18.12 ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 17.73/18.12 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha2( X, Y, Z ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 17.73/18.12 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 17.73/18.12 sdtasdt0( Z, X ) ) }.
% 17.73/18.12 { ! alpha2( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 17.73/18.12 { ! alpha2( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 17.73/18.12 { ! alpha2( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 17.73/18.12 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 17.73/18.12 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha2( X, Y, Z
% 17.73/18.12 ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 17.73/18.12 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 17.73/18.12 sdtasdt0( Y, X ) ) }.
% 17.73/18.12 { && }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 17.73/18.12 ), iLess0( X, Y ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 17.73/18.12 aNaturalNumber0( skol2( Z, T ) ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 17.73/18.12 sdtasdt0( X, skol2( X, Y ) ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 17.73/18.12 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 17.73/18.12 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 17.73/18.12 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 17.73/18.12 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 17.73/18.12 ) }.
% 17.73/18.12 { aNaturalNumber0( xl ) }.
% 17.73/18.12 { aNaturalNumber0( xm ) }.
% 17.73/18.12 { aNaturalNumber0( xn ) }.
% 17.73/18.12 { aNaturalNumber0( skol3 ) }.
% 17.73/18.12 { xm = sdtasdt0( xl, skol3 ) }.
% 17.73/18.12 { doDivides0( xl, xm ) }.
% 17.73/18.12 { aNaturalNumber0( skol4 ) }.
% 17.73/18.12 { xn = sdtasdt0( xm, skol4 ) }.
% 17.73/18.12 { doDivides0( xm, xn ) }.
% 17.73/18.12 { ! aNaturalNumber0( X ), ! xn = sdtasdt0( xl, X ) }.
% 17.73/18.12 { ! doDivides0( xl, xn ) }.
% 17.73/18.12
% 17.73/18.12 percentage equality = 0.309322, percentage horn = 0.753623
% 17.73/18.12 This is a problem with some equality
% 17.73/18.12
% 17.73/18.12
% 17.73/18.12
% 17.73/18.12 Options Used:
% 17.73/18.12
% 17.73/18.12 useres = 1
% 17.73/18.12 useparamod = 1
% 17.73/18.12 useeqrefl = 1
% 17.73/18.12 useeqfact = 1
% 17.73/18.12 usefactor = 1
% 17.73/18.12 usesimpsplitting = 0
% 17.73/18.12 usesimpdemod = 5
% 17.73/18.12 usesimpres = 3
% 17.73/18.12
% 17.73/18.12 resimpinuse = 1000
% 17.73/18.12 resimpclauses = 20000
% 17.73/18.12 substype = eqrewr
% 17.73/18.12 backwardsubs = 1
% 17.73/18.12 selectoldest = 5
% 17.73/18.12
% 17.73/18.12 litorderings [0] = split
% 17.73/18.12 litorderings [1] = extend the termordering, first sorting on arguments
% 17.73/18.12
% 17.73/18.12 termordering = kbo
% 17.73/18.12
% 17.73/18.12 litapriori = 0
% 17.73/18.12 termapriori = 1
% 17.73/18.12 litaposteriori = 0
% 17.73/18.12 termaposteriori = 0
% 17.73/18.12 demodaposteriori = 0
% 17.73/18.12 ordereqreflfact = 0
% 17.73/18.12
% 17.73/18.12 litselect = negord
% 17.73/18.12
% 17.73/18.12 maxweight = 15
% 17.73/18.12 maxdepth = 30000
% 17.73/18.12 maxlength = 115
% 17.73/18.12 maxnrvars = 195
% 17.73/18.12 excuselevel = 1
% 17.73/18.12 increasemaxweight = 1
% 17.73/18.12
% 17.73/18.12 maxselected = 10000000
% 17.73/18.12 maxnrclauses = 10000000
% 17.73/18.12
% 17.73/18.12 showgenerated = 0
% 17.73/18.12 showkept = 0
% 17.73/18.12 showselected = 0
% 17.73/18.12 showdeleted = 0
% 17.73/18.12 showresimp = 1
% 17.73/18.12 showstatus = 2000
% 17.73/18.12
% 17.73/18.12 prologoutput = 0
% 17.73/18.12 nrgoals = 5000000
% 17.73/18.12 totalproof = 1
% 17.73/18.12
% 17.73/18.12 Symbols occurring in the translation:
% 17.73/18.12
% 17.73/18.12 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 17.73/18.12 . [1, 2] (w:1, o:22, a:1, s:1, b:0),
% 17.73/18.12 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 17.73/18.12 ! [4, 1] (w:0, o:16, a:1, s:1, b:0),
% 17.73/18.12 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.73/18.12 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 17.73/18.12 aNaturalNumber0 [36, 1] (w:1, o:21, a:1, s:1, b:0),
% 17.73/18.12 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 17.73/18.12 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 17.73/18.12 sdtpldt0 [40, 2] (w:1, o:46, a:1, s:1, b:0),
% 17.73/18.12 sdtasdt0 [41, 2] (w:1, o:47, a:1, s:1, b:0),
% 17.73/18.12 sdtlseqdt0 [43, 2] (w:1, o:48, a:1, s:1, b:0),
% 17.73/18.12 sdtmndt0 [44, 2] (w:1, o:49, a:1, s:1, b:0),
% 17.73/18.12 iLess0 [45, 2] (w:1, o:50, a:1, s:1, b:0),
% 48.24/48.61 doDivides0 [46, 2] (w:1, o:51, a:1, s:1, b:0),
% 48.24/48.61 sdtsldt0 [47, 2] (w:1, o:52, a:1, s:1, b:0),
% 48.24/48.61 xl [48, 0] (w:1, o:11, a:1, s:1, b:0),
% 48.24/48.61 xm [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 48.24/48.61 xn [50, 0] (w:1, o:13, a:1, s:1, b:0),
% 48.24/48.61 alpha1 [51, 3] (w:1, o:55, a:1, s:1, b:1),
% 48.24/48.61 alpha2 [52, 3] (w:1, o:56, a:1, s:1, b:1),
% 48.24/48.61 skol1 [53, 2] (w:1, o:53, a:1, s:1, b:1),
% 48.24/48.61 skol2 [54, 2] (w:1, o:54, a:1, s:1, b:1),
% 48.24/48.61 skol3 [55, 0] (w:1, o:14, a:1, s:1, b:1),
% 48.24/48.61 skol4 [56, 0] (w:1, o:15, a:1, s:1, b:1).
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Starting Search:
% 48.24/48.61
% 48.24/48.61 *** allocated 15000 integers for clauses
% 48.24/48.61 *** allocated 22500 integers for clauses
% 48.24/48.61 *** allocated 33750 integers for clauses
% 48.24/48.61 *** allocated 50625 integers for clauses
% 48.24/48.61 *** allocated 15000 integers for termspace/termends
% 48.24/48.61 *** allocated 75937 integers for clauses
% 48.24/48.61 *** allocated 22500 integers for termspace/termends
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 113905 integers for clauses
% 48.24/48.61 *** allocated 33750 integers for termspace/termends
% 48.24/48.61 *** allocated 170857 integers for clauses
% 48.24/48.61 *** allocated 50625 integers for termspace/termends
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 12957
% 48.24/48.61 Kept: 2102
% 48.24/48.61 Inuse: 125
% 48.24/48.61 Deleted: 11
% 48.24/48.61 Deletedinuse: 5
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 75937 integers for termspace/termends
% 48.24/48.61 *** allocated 256285 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 26431
% 48.24/48.61 Kept: 4105
% 48.24/48.61 Inuse: 180
% 48.24/48.61 Deleted: 21
% 48.24/48.61 Deletedinuse: 11
% 48.24/48.61
% 48.24/48.61 *** allocated 113905 integers for termspace/termends
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 384427 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 170857 integers for termspace/termends
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 47075
% 48.24/48.61 Kept: 6119
% 48.24/48.61 Inuse: 211
% 48.24/48.61 Deleted: 27
% 48.24/48.61 Deletedinuse: 11
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 576640 integers for clauses
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 59505
% 48.24/48.61 Kept: 8221
% 48.24/48.61 Inuse: 244
% 48.24/48.61 Deleted: 29
% 48.24/48.61 Deletedinuse: 12
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 256285 integers for termspace/termends
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 84387
% 48.24/48.61 Kept: 10224
% 48.24/48.61 Inuse: 319
% 48.24/48.61 Deleted: 45
% 48.24/48.61 Deletedinuse: 21
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 864960 integers for clauses
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 118901
% 48.24/48.61 Kept: 12231
% 48.24/48.61 Inuse: 412
% 48.24/48.61 Deleted: 53
% 48.24/48.61 Deletedinuse: 21
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 384427 integers for termspace/termends
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 133810
% 48.24/48.61 Kept: 14512
% 48.24/48.61 Inuse: 468
% 48.24/48.61 Deleted: 91
% 48.24/48.61 Deletedinuse: 33
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 155407
% 48.24/48.61 Kept: 16512
% 48.24/48.61 Inuse: 506
% 48.24/48.61 Deleted: 91
% 48.24/48.61 Deletedinuse: 33
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 1297440 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 183891
% 48.24/48.61 Kept: 18620
% 48.24/48.61 Inuse: 547
% 48.24/48.61 Deleted: 97
% 48.24/48.61 Deletedinuse: 34
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying clauses:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 214110
% 48.24/48.61 Kept: 22143
% 48.24/48.61 Inuse: 582
% 48.24/48.61 Deleted: 4854
% 48.24/48.61 Deletedinuse: 35
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 576640 integers for termspace/termends
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 233840
% 48.24/48.61 Kept: 24215
% 48.24/48.61 Inuse: 636
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 251254
% 48.24/48.61 Kept: 26658
% 48.24/48.61 Inuse: 659
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 1946160 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 265895
% 48.24/48.61 Kept: 28783
% 48.24/48.61 Inuse: 694
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 276440
% 48.24/48.61 Kept: 31579
% 48.24/48.61 Inuse: 714
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 285092
% 48.24/48.61 Kept: 34422
% 48.24/48.61 Inuse: 729
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 301573
% 48.24/48.61 Kept: 36502
% 48.24/48.61 Inuse: 769
% 48.24/48.61 Deleted: 4873
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 864960 integers for termspace/termends
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 316260
% 48.24/48.61 Kept: 38565
% 48.24/48.61 Inuse: 807
% 48.24/48.61 Deleted: 4875
% 48.24/48.61 Deletedinuse: 54
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 2919240 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 338357
% 48.24/48.61 Kept: 40572
% 48.24/48.61 Inuse: 856
% 48.24/48.61 Deleted: 4942
% 48.24/48.61 Deletedinuse: 113
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying clauses:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 358608
% 48.24/48.61 Kept: 43544
% 48.24/48.61 Inuse: 892
% 48.24/48.61 Deleted: 13528
% 48.24/48.61 Deletedinuse: 126
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 369189
% 48.24/48.61 Kept: 45604
% 48.24/48.61 Inuse: 923
% 48.24/48.61 Deleted: 13537
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 381540
% 48.24/48.61 Kept: 47643
% 48.24/48.61 Inuse: 957
% 48.24/48.61 Deleted: 13537
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 409365
% 48.24/48.61 Kept: 49715
% 48.24/48.61 Inuse: 1030
% 48.24/48.61 Deleted: 13537
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 440685
% 48.24/48.61 Kept: 51723
% 48.24/48.61 Inuse: 1098
% 48.24/48.61 Deleted: 13538
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 469462
% 48.24/48.61 Kept: 53742
% 48.24/48.61 Inuse: 1189
% 48.24/48.61 Deleted: 13538
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 489115
% 48.24/48.61 Kept: 55795
% 48.24/48.61 Inuse: 1235
% 48.24/48.61 Deleted: 13538
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 506992
% 48.24/48.61 Kept: 57798
% 48.24/48.61 Inuse: 1287
% 48.24/48.61 Deleted: 13538
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 *** allocated 4378860 integers for clauses
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 *** allocated 1297440 integers for termspace/termends
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 525482
% 48.24/48.61 Kept: 59872
% 48.24/48.61 Inuse: 1332
% 48.24/48.61 Deleted: 13543
% 48.24/48.61 Deletedinuse: 135
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Intermediate Status:
% 48.24/48.61 Generated: 559826
% 48.24/48.61 Kept: 61930
% 48.24/48.61 Inuse: 1458
% 48.24/48.61 Deleted: 13588
% 48.24/48.61 Deletedinuse: 176
% 48.24/48.61
% 48.24/48.61 Resimplifying inuse:
% 48.24/48.61 Done
% 48.24/48.61
% 48.24/48.61 Resimplifying clauses:
% 48.24/48.61
% 48.24/48.61 Bliksems!, er is een bewijs:
% 48.24/48.61 % SZS status Theorem
% 48.24/48.61 % SZS output start Refutation
% 48.24/48.61
% 48.24/48.61 (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 48.24/48.61 , aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 48.24/48.61 (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 48.24/48.61 ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.61 (11) {G0,W17,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 48.24/48.61 ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtasdt0( Y, Z ) ) ==> sdtasdt0
% 48.24/48.61 ( sdtasdt0( X, Y ), Z ) }.
% 48.24/48.61 (58) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 48.24/48.61 (59) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 48.24/48.61 (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol3 ) }.
% 48.24/48.61 (62) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, skol3 ) ==> xm }.
% 48.24/48.61 (64) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol4 ) }.
% 48.24/48.61 (65) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xm, skol4 ) ==> xn }.
% 48.24/48.61 (67) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), ! sdtasdt0( xl, X )
% 48.24/48.61 ==> xn }.
% 48.24/48.61 (227) {G1,W6,D3,L2,V1,M2} R(5,61) { ! aNaturalNumber0( X ), aNaturalNumber0
% 48.24/48.61 ( sdtasdt0( X, skol3 ) ) }.
% 48.24/48.61 (432) {G1,W9,D3,L2,V1,M2} R(10,58) { ! aNaturalNumber0( X ), sdtasdt0( xl,
% 48.24/48.61 X ) = sdtasdt0( X, xl ) }.
% 48.24/48.61 (437) {G1,W7,D3,L2,V0,M2} P(10,62);r(58) { sdtasdt0( skol3, xl ) ==> xm, !
% 48.24/48.61 aNaturalNumber0( skol3 ) }.
% 48.24/48.61 (438) {G1,W7,D3,L2,V0,M2} P(10,65);r(59) { sdtasdt0( skol4, xm ) ==> xn, !
% 48.24/48.61 aNaturalNumber0( skol4 ) }.
% 48.24/48.61 (467) {G1,W15,D4,L3,V2,M3} R(11,64) { ! aNaturalNumber0( X ), !
% 48.24/48.61 aNaturalNumber0( Y ), sdtasdt0( skol4, sdtasdt0( X, Y ) ) ==> sdtasdt0(
% 48.24/48.61 sdtasdt0( skol4, X ), Y ) }.
% 48.24/48.61 (5543) {G2,W4,D3,L1,V0,M1} R(227,64) { aNaturalNumber0( sdtasdt0( skol4,
% 48.24/48.61 skol3 ) ) }.
% 48.24/48.61 (9416) {G3,W7,D4,L1,V0,M1} R(67,5543) { ! sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.61 skol3 ) ) ==> xn }.
% 48.24/48.61 (22116) {G2,W5,D3,L1,V0,M1} S(437);r(61) { sdtasdt0( skol3, xl ) ==> xm }.
% 48.24/48.61 (22117) {G2,W5,D3,L1,V0,M1} S(438);r(64) { sdtasdt0( skol4, xm ) ==> xn }.
% 48.24/48.61 (60612) {G3,W11,D4,L1,V0,M1} R(432,5543) { sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.61 skol3 ) ) ==> sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) }.
% 48.24/48.61 (63071) {G3,W9,D4,L2,V0,M2} P(22116,467);d(22117);r(61) { ! aNaturalNumber0
% 48.24/48.61 ( xl ), sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) ==> xn }.
% 48.24/48.61 (63583) {G4,W7,D4,L1,V0,M1} S(63071);r(58) { sdtasdt0( sdtasdt0( skol4,
% 48.24/48.61 skol3 ), xl ) ==> xn }.
% 48.24/48.61 (63808) {G5,W0,D0,L0,V0,M0} S(60612);d(63583);r(9416) { }.
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 % SZS output end Refutation
% 48.24/48.61 found a proof!
% 48.24/48.61
% 48.24/48.61
% 48.24/48.61 Unprocessed initial clauses:
% 48.24/48.61
% 48.24/48.61 (63810) {G0,W1,D1,L1,V0,M1} { && }.
% 48.24/48.61 (63811) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 48.24/48.61 (63812) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 48.24/48.61 (63813) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 48.24/48.61 (63814) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 48.24/48.61 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 48.24/48.61 (63815) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 48.24/48.61 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 48.24/48.61 (63816) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 48.24/48.61 (63817) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 48.24/48.61 X, sdtpldt0( Y, Z ) ) }.
% 48.24/48.61 (63818) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 48.24/48.61 = X }.
% 48.24/48.61 (63819) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 48.24/48.61 X ) }.
% 48.24/48.61 (63820) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.61 (63821) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 48.24/48.61 X, sdtasdt0( Y, Z ) ) }.
% 48.24/48.61 (63822) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 48.24/48.61 = X }.
% 48.24/48.61 (63823) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 48.24/48.61 X ) }.
% 48.24/48.61 (63824) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 48.24/48.61 = sz00 }.
% 48.24/48.61 (63825) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 48.24/48.61 sz00, X ) }.
% 48.24/48.61 (63826) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 48.24/48.61 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 48.24/48.61 (63827) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 48.24/48.61 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 48.24/48.61 (63828) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 48.24/48.61 }.
% 48.24/48.61 (63829) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 48.24/48.61 }.
% 48.24/48.61 (63830) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 48.24/48.61 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 48.24/48.61 sdtasdt0( X, Z ), Y = Z }.
% 48.24/48.61 (63831) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 48.24/48.61 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 48.24/48.61 sdtasdt0( Z, X ), Y = Z }.
% 48.24/48.61 (63832) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 48.24/48.61 (63833) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 48.24/48.61 (63834) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 48.24/48.61 (63835) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 48.24/48.61 (63836) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 48.24/48.61 (63837) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 48.24/48.61 }.
% 48.24/48.61 (63838) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 48.24/48.61 }.
% 48.24/48.61 (63839) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 48.24/48.61 }.
% 48.24/48.61 (63840) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 48.24/48.61 , Z = sdtmndt0( Y, X ) }.
% 48.24/48.61 (63841) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 48.24/48.61 }.
% 48.24/48.61 (63842) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 48.24/48.61 (63843) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 48.24/48.61 sdtlseqdt0( X, Z ) }.
% 48.24/48.61 (63844) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 48.24/48.61 (63845) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 48.24/48.61 (63846) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha1( X, Y, Z
% 48.24/48.61 ) }.
% 48.24/48.61 (63847) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 48.24/48.61 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 48.24/48.61 (63848) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 48.24/48.61 sdtpldt0( Z, Y ) }.
% 48.24/48.61 (63849) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 48.24/48.61 Z, X ), sdtpldt0( Z, Y ) ) }.
% 48.24/48.61 (63850) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 48.24/48.61 sdtpldt0( Y, Z ) }.
% 48.24/48.61 (63851) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 48.24/48.61 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 48.24/48.61 sdtpldt0( Y, Z ), alpha1( X, Y, Z ) }.
% 48.24/48.61 (63852) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 48.24/48.61 alpha2( X, Y, Z ) }.
% 48.24/48.61 (63853) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 48.24/48.61 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 48.24/48.61 (63854) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 48.24/48.61 sdtasdt0( X, Z ) }.
% 48.24/48.61 (63855) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 48.24/48.61 X, Y ), sdtasdt0( X, Z ) ) }.
% 48.24/48.61 (63856) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 48.24/48.61 sdtasdt0( Z, X ) }.
% 48.24/48.61 (63857) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 48.24/48.61 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 48.24/48.61 sdtasdt0( Z, X ), alpha2( X, Y, Z ) }.
% 48.24/48.61 (63858) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 48.24/48.61 , ! sz10 = X }.
% 48.24/48.61 (63859) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 48.24/48.61 , sdtlseqdt0( sz10, X ) }.
% 48.24/48.61 (63860) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 48.24/48.61 (63861) {G0,W1,D1,L1,V0,M1} { && }.
% 48.24/48.61 (63862) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 48.24/48.61 (63863) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 48.24/48.61 (63864) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 48.24/48.61 (63865) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 48.24/48.61 }.
% 48.24/48.61 (63866) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.61 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 48.24/48.61 aNaturalNumber0( Z ) }.
% 48.24/48.62 (63867) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.62 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 48.24/48.62 ( X, Z ) }.
% 48.24/48.62 (63868) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 48.24/48.62 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 48.24/48.62 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 48.24/48.62 (63869) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 48.24/48.62 (63870) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 48.24/48.62 (63871) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 48.24/48.62 (63872) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol3 ) }.
% 48.24/48.62 (63873) {G0,W5,D3,L1,V0,M1} { xm = sdtasdt0( xl, skol3 ) }.
% 48.24/48.62 (63874) {G0,W3,D2,L1,V0,M1} { doDivides0( xl, xm ) }.
% 48.24/48.62 (63875) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol4 ) }.
% 48.24/48.62 (63876) {G0,W5,D3,L1,V0,M1} { xn = sdtasdt0( xm, skol4 ) }.
% 48.24/48.62 (63877) {G0,W3,D2,L1,V0,M1} { doDivides0( xm, xn ) }.
% 48.24/48.62 (63878) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), ! xn = sdtasdt0( xl
% 48.24/48.62 , X ) }.
% 48.24/48.62 (63879) {G0,W3,D2,L1,V0,M1} { ! doDivides0( xl, xn ) }.
% 48.24/48.62
% 48.24/48.62
% 48.24/48.62 Total Proof:
% 48.24/48.62
% 48.24/48.62 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 48.24/48.62 parent0: (63815) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 X := X
% 48.24/48.62 Y := Y
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 1 ==> 1
% 48.24/48.62 2 ==> 2
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.62 parent0: (63820) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 X := X
% 48.24/48.62 Y := Y
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 1 ==> 1
% 48.24/48.62 2 ==> 2
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 eqswap: (63915) {G0,W17,D4,L4,V3,M4} { sdtasdt0( X, sdtasdt0( Y, Z ) ) =
% 48.24/48.62 sdtasdt0( sdtasdt0( X, Y ), Z ), ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 48.24/48.62 parent0[3]: (63821) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y )
% 48.24/48.62 , Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 X := X
% 48.24/48.62 Y := Y
% 48.24/48.62 Z := Z
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (11) {G0,W17,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtasdt0( Y, Z
% 48.24/48.62 ) ) ==> sdtasdt0( sdtasdt0( X, Y ), Z ) }.
% 48.24/48.62 parent0: (63915) {G0,W17,D4,L4,V3,M4} { sdtasdt0( X, sdtasdt0( Y, Z ) ) =
% 48.24/48.62 sdtasdt0( sdtasdt0( X, Y ), Z ), ! aNaturalNumber0( X ), !
% 48.24/48.62 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 X := X
% 48.24/48.62 Y := Y
% 48.24/48.62 Z := Z
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 3
% 48.24/48.62 1 ==> 0
% 48.24/48.62 2 ==> 1
% 48.24/48.62 3 ==> 2
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (58) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 48.24/48.62 parent0: (63869) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (59) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 48.24/48.62 parent0: (63870) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol3 ) }.
% 48.24/48.62 parent0: (63872) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol3 ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 eqswap: (65368) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xl, skol3 ) = xm }.
% 48.24/48.62 parent0[0]: (63873) {G0,W5,D3,L1,V0,M1} { xm = sdtasdt0( xl, skol3 ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (62) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, skol3 ) ==> xm }.
% 48.24/48.62 parent0: (65368) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xl, skol3 ) = xm }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (64) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol4 ) }.
% 48.24/48.62 parent0: (63875) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol4 ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.62 0 ==> 0
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 eqswap: (66093) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xm, skol4 ) = xn }.
% 48.24/48.62 parent0[0]: (63876) {G0,W5,D3,L1,V0,M1} { xn = sdtasdt0( xm, skol4 ) }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62
% 48.24/48.62 subsumption: (65) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xm, skol4 ) ==> xn }.
% 48.24/48.62 parent0: (66093) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xm, skol4 ) = xn }.
% 48.24/48.62 substitution0:
% 48.24/48.62 end
% 48.24/48.62 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66457) {G0,W7,D3,L2,V1,M2} { ! sdtasdt0( xl, X ) = xn, !
% 48.24/48.63 aNaturalNumber0( X ) }.
% 48.24/48.63 parent0[1]: (63878) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), ! xn =
% 48.24/48.63 sdtasdt0( xl, X ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (67) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 sdtasdt0( xl, X ) ==> xn }.
% 48.24/48.63 parent0: (66457) {G0,W7,D3,L2,V1,M2} { ! sdtasdt0( xl, X ) = xn, !
% 48.24/48.63 aNaturalNumber0( X ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 1
% 48.24/48.63 1 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66459) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 48.24/48.63 aNaturalNumber0( sdtasdt0( X, skol3 ) ) }.
% 48.24/48.63 parent0[1]: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 48.24/48.63 parent1[0]: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol3 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 Y := skol3
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (227) {G1,W6,D3,L2,V1,M2} R(5,61) { ! aNaturalNumber0( X ),
% 48.24/48.63 aNaturalNumber0( sdtasdt0( X, skol3 ) ) }.
% 48.24/48.63 parent0: (66459) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 48.24/48.63 aNaturalNumber0( sdtasdt0( X, skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 1 ==> 1
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66460) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0
% 48.24/48.63 ( xl, X ) = sdtasdt0( X, xl ) }.
% 48.24/48.63 parent0[0]: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.63 parent1[0]: (58) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := xl
% 48.24/48.63 Y := X
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (432) {G1,W9,D3,L2,V1,M2} R(10,58) { ! aNaturalNumber0( X ),
% 48.24/48.63 sdtasdt0( xl, X ) = sdtasdt0( X, xl ) }.
% 48.24/48.63 parent0: (66460) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0(
% 48.24/48.63 xl, X ) = sdtasdt0( X, xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 1 ==> 1
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66462) {G0,W5,D3,L1,V0,M1} { xm ==> sdtasdt0( xl, skol3 ) }.
% 48.24/48.63 parent0[0]: (62) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, skol3 ) ==> xm }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 paramod: (66463) {G1,W9,D3,L3,V0,M3} { xm ==> sdtasdt0( skol3, xl ), !
% 48.24/48.63 aNaturalNumber0( xl ), ! aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent0[2]: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.63 parent1[0; 2]: (66462) {G0,W5,D3,L1,V0,M1} { xm ==> sdtasdt0( xl, skol3 )
% 48.24/48.63 }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := xl
% 48.24/48.63 Y := skol3
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66503) {G1,W7,D3,L2,V0,M2} { xm ==> sdtasdt0( skol3, xl ), !
% 48.24/48.63 aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent0[1]: (66463) {G1,W9,D3,L3,V0,M3} { xm ==> sdtasdt0( skol3, xl ), !
% 48.24/48.63 aNaturalNumber0( xl ), ! aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent1[0]: (58) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66504) {G1,W7,D3,L2,V0,M2} { sdtasdt0( skol3, xl ) ==> xm, !
% 48.24/48.63 aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent0[0]: (66503) {G1,W7,D3,L2,V0,M2} { xm ==> sdtasdt0( skol3, xl ), !
% 48.24/48.63 aNaturalNumber0( skol3 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (437) {G1,W7,D3,L2,V0,M2} P(10,62);r(58) { sdtasdt0( skol3, xl
% 48.24/48.63 ) ==> xm, ! aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent0: (66504) {G1,W7,D3,L2,V0,M2} { sdtasdt0( skol3, xl ) ==> xm, !
% 48.24/48.63 aNaturalNumber0( skol3 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 1 ==> 1
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66505) {G0,W5,D3,L1,V0,M1} { xn ==> sdtasdt0( xm, skol4 ) }.
% 48.24/48.63 parent0[0]: (65) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xm, skol4 ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 paramod: (66506) {G1,W9,D3,L3,V0,M3} { xn ==> sdtasdt0( skol4, xm ), !
% 48.24/48.63 aNaturalNumber0( xm ), ! aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent0[2]: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 48.24/48.63 parent1[0; 2]: (66505) {G0,W5,D3,L1,V0,M1} { xn ==> sdtasdt0( xm, skol4 )
% 48.24/48.63 }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := xm
% 48.24/48.63 Y := skol4
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66546) {G1,W7,D3,L2,V0,M2} { xn ==> sdtasdt0( skol4, xm ), !
% 48.24/48.63 aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent0[1]: (66506) {G1,W9,D3,L3,V0,M3} { xn ==> sdtasdt0( skol4, xm ), !
% 48.24/48.63 aNaturalNumber0( xm ), ! aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent1[0]: (59) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66547) {G1,W7,D3,L2,V0,M2} { sdtasdt0( skol4, xm ) ==> xn, !
% 48.24/48.63 aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent0[0]: (66546) {G1,W7,D3,L2,V0,M2} { xn ==> sdtasdt0( skol4, xm ), !
% 48.24/48.63 aNaturalNumber0( skol4 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (438) {G1,W7,D3,L2,V0,M2} P(10,65);r(59) { sdtasdt0( skol4, xm
% 48.24/48.63 ) ==> xn, ! aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent0: (66547) {G1,W7,D3,L2,V0,M2} { sdtasdt0( skol4, xm ) ==> xn, !
% 48.24/48.63 aNaturalNumber0( skol4 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 1 ==> 1
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66548) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z ) ==>
% 48.24/48.63 sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 48.24/48.63 parent0[3]: (11) {G0,W17,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtasdt0( Y, Z
% 48.24/48.63 ) ) ==> sdtasdt0( sdtasdt0( X, Y ), Z ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 Y := Y
% 48.24/48.63 Z := Z
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66549) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( skol4, X )
% 48.24/48.63 , Y ) ==> sdtasdt0( skol4, sdtasdt0( X, Y ) ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ) }.
% 48.24/48.63 parent0[1]: (66548) {G0,W17,D4,L4,V3,M4} { sdtasdt0( sdtasdt0( X, Y ), Z )
% 48.24/48.63 ==> sdtasdt0( X, sdtasdt0( Y, Z ) ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 48.24/48.63 parent1[0]: (64) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol4 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := skol4
% 48.24/48.63 Y := X
% 48.24/48.63 Z := Y
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66554) {G1,W15,D4,L3,V2,M3} { sdtasdt0( skol4, sdtasdt0( X, Y ) )
% 48.24/48.63 ==> sdtasdt0( sdtasdt0( skol4, X ), Y ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ) }.
% 48.24/48.63 parent0[0]: (66549) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( skol4, X )
% 48.24/48.63 , Y ) ==> sdtasdt0( skol4, sdtasdt0( X, Y ) ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 Y := Y
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (467) {G1,W15,D4,L3,V2,M3} R(11,64) { ! aNaturalNumber0( X ),
% 48.24/48.63 ! aNaturalNumber0( Y ), sdtasdt0( skol4, sdtasdt0( X, Y ) ) ==> sdtasdt0
% 48.24/48.63 ( sdtasdt0( skol4, X ), Y ) }.
% 48.24/48.63 parent0: (66554) {G1,W15,D4,L3,V2,M3} { sdtasdt0( skol4, sdtasdt0( X, Y )
% 48.24/48.63 ) ==> sdtasdt0( sdtasdt0( skol4, X ), Y ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 Y := Y
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 2
% 48.24/48.63 1 ==> 0
% 48.24/48.63 2 ==> 1
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66561) {G1,W4,D3,L1,V0,M1} { aNaturalNumber0( sdtasdt0( skol4
% 48.24/48.63 , skol3 ) ) }.
% 48.24/48.63 parent0[0]: (227) {G1,W6,D3,L2,V1,M2} R(5,61) { ! aNaturalNumber0( X ),
% 48.24/48.63 aNaturalNumber0( sdtasdt0( X, skol3 ) ) }.
% 48.24/48.63 parent1[0]: (64) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol4 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := skol4
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (5543) {G2,W4,D3,L1,V0,M1} R(227,64) { aNaturalNumber0(
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) }.
% 48.24/48.63 parent0: (66561) {G1,W4,D3,L1,V0,M1} { aNaturalNumber0( sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66562) {G0,W7,D3,L2,V1,M2} { ! xn ==> sdtasdt0( xl, X ), !
% 48.24/48.63 aNaturalNumber0( X ) }.
% 48.24/48.63 parent0[1]: (67) {G0,W7,D3,L2,V1,M2} I { ! aNaturalNumber0( X ), ! sdtasdt0
% 48.24/48.63 ( xl, X ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66563) {G1,W7,D4,L1,V0,M1} { ! xn ==> sdtasdt0( xl, sdtasdt0
% 48.24/48.63 ( skol4, skol3 ) ) }.
% 48.24/48.63 parent0[1]: (66562) {G0,W7,D3,L2,V1,M2} { ! xn ==> sdtasdt0( xl, X ), !
% 48.24/48.63 aNaturalNumber0( X ) }.
% 48.24/48.63 parent1[0]: (5543) {G2,W4,D3,L1,V0,M1} R(227,64) { aNaturalNumber0(
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := sdtasdt0( skol4, skol3 )
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66564) {G1,W7,D4,L1,V0,M1} { ! sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) ==> xn }.
% 48.24/48.63 parent0[0]: (66563) {G1,W7,D4,L1,V0,M1} { ! xn ==> sdtasdt0( xl, sdtasdt0
% 48.24/48.63 ( skol4, skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (9416) {G3,W7,D4,L1,V0,M1} R(67,5543) { ! sdtasdt0( xl,
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) ==> xn }.
% 48.24/48.63 parent0: (66564) {G1,W7,D4,L1,V0,M1} { ! sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66566) {G1,W5,D3,L1,V0,M1} { sdtasdt0( skol3, xl ) ==> xm }.
% 48.24/48.63 parent0[1]: (437) {G1,W7,D3,L2,V0,M2} P(10,62);r(58) { sdtasdt0( skol3, xl
% 48.24/48.63 ) ==> xm, ! aNaturalNumber0( skol3 ) }.
% 48.24/48.63 parent1[0]: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol3 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (22116) {G2,W5,D3,L1,V0,M1} S(437);r(61) { sdtasdt0( skol3, xl
% 48.24/48.63 ) ==> xm }.
% 48.24/48.63 parent0: (66566) {G1,W5,D3,L1,V0,M1} { sdtasdt0( skol3, xl ) ==> xm }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66569) {G1,W5,D3,L1,V0,M1} { sdtasdt0( skol4, xm ) ==> xn }.
% 48.24/48.63 parent0[1]: (438) {G1,W7,D3,L2,V0,M2} P(10,65);r(59) { sdtasdt0( skol4, xm
% 48.24/48.63 ) ==> xn, ! aNaturalNumber0( skol4 ) }.
% 48.24/48.63 parent1[0]: (64) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol4 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (22117) {G2,W5,D3,L1,V0,M1} S(438);r(64) { sdtasdt0( skol4, xm
% 48.24/48.63 ) ==> xn }.
% 48.24/48.63 parent0: (66569) {G1,W5,D3,L1,V0,M1} { sdtasdt0( skol4, xm ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66571) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl, X
% 48.24/48.63 ), ! aNaturalNumber0( X ) }.
% 48.24/48.63 parent0[1]: (432) {G1,W9,D3,L2,V1,M2} R(10,58) { ! aNaturalNumber0( X ),
% 48.24/48.63 sdtasdt0( xl, X ) = sdtasdt0( X, xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66572) {G2,W11,D4,L1,V0,M1} { sdtasdt0( sdtasdt0( skol4,
% 48.24/48.63 skol3 ), xl ) = sdtasdt0( xl, sdtasdt0( skol4, skol3 ) ) }.
% 48.24/48.63 parent0[1]: (66571) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl
% 48.24/48.63 , X ), ! aNaturalNumber0( X ) }.
% 48.24/48.63 parent1[0]: (5543) {G2,W4,D3,L1,V0,M1} R(227,64) { aNaturalNumber0(
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := sdtasdt0( skol4, skol3 )
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66573) {G2,W11,D4,L1,V0,M1} { sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) = sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) }.
% 48.24/48.63 parent0[0]: (66572) {G2,W11,D4,L1,V0,M1} { sdtasdt0( sdtasdt0( skol4,
% 48.24/48.63 skol3 ), xl ) = sdtasdt0( xl, sdtasdt0( skol4, skol3 ) ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (60612) {G3,W11,D4,L1,V0,M1} R(432,5543) { sdtasdt0( xl,
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) ==> sdtasdt0( sdtasdt0( skol4, skol3 ), xl )
% 48.24/48.63 }.
% 48.24/48.63 parent0: (66573) {G2,W11,D4,L1,V0,M1} { sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) = sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 eqswap: (66575) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( skol4, X ), Y )
% 48.24/48.63 ==> sdtasdt0( skol4, sdtasdt0( X, Y ) ), ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ) }.
% 48.24/48.63 parent0[2]: (467) {G1,W15,D4,L3,V2,M3} R(11,64) { ! aNaturalNumber0( X ), !
% 48.24/48.63 aNaturalNumber0( Y ), sdtasdt0( skol4, sdtasdt0( X, Y ) ) ==> sdtasdt0(
% 48.24/48.63 sdtasdt0( skol4, X ), Y ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 X := X
% 48.24/48.63 Y := Y
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 paramod: (66577) {G2,W13,D4,L3,V0,M3} { sdtasdt0( sdtasdt0( skol4, skol3 )
% 48.24/48.63 , xl ) ==> sdtasdt0( skol4, xm ), ! aNaturalNumber0( skol3 ), !
% 48.24/48.63 aNaturalNumber0( xl ) }.
% 48.24/48.63 parent0[0]: (22116) {G2,W5,D3,L1,V0,M1} S(437);r(61) { sdtasdt0( skol3, xl
% 48.24/48.63 ) ==> xm }.
% 48.24/48.63 parent1[0; 8]: (66575) {G1,W15,D4,L3,V2,M3} { sdtasdt0( sdtasdt0( skol4, X
% 48.24/48.63 ), Y ) ==> sdtasdt0( skol4, sdtasdt0( X, Y ) ), ! aNaturalNumber0( X ),
% 48.24/48.63 ! aNaturalNumber0( Y ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 X := skol3
% 48.24/48.63 Y := xl
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 paramod: (66578) {G3,W11,D4,L3,V0,M3} { sdtasdt0( sdtasdt0( skol4, skol3 )
% 48.24/48.63 , xl ) ==> xn, ! aNaturalNumber0( skol3 ), ! aNaturalNumber0( xl ) }.
% 48.24/48.63 parent0[0]: (22117) {G2,W5,D3,L1,V0,M1} S(438);r(64) { sdtasdt0( skol4, xm
% 48.24/48.63 ) ==> xn }.
% 48.24/48.63 parent1[0; 6]: (66577) {G2,W13,D4,L3,V0,M3} { sdtasdt0( sdtasdt0( skol4,
% 48.24/48.63 skol3 ), xl ) ==> sdtasdt0( skol4, xm ), ! aNaturalNumber0( skol3 ), !
% 48.24/48.63 aNaturalNumber0( xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66579) {G1,W9,D4,L2,V0,M2} { sdtasdt0( sdtasdt0( skol4, skol3
% 48.24/48.63 ), xl ) ==> xn, ! aNaturalNumber0( xl ) }.
% 48.24/48.63 parent0[1]: (66578) {G3,W11,D4,L3,V0,M3} { sdtasdt0( sdtasdt0( skol4,
% 48.24/48.63 skol3 ), xl ) ==> xn, ! aNaturalNumber0( skol3 ), ! aNaturalNumber0( xl )
% 48.24/48.63 }.
% 48.24/48.63 parent1[0]: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol3 ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (63071) {G3,W9,D4,L2,V0,M2} P(22116,467);d(22117);r(61) { !
% 48.24/48.63 aNaturalNumber0( xl ), sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) ==> xn
% 48.24/48.63 }.
% 48.24/48.63 parent0: (66579) {G1,W9,D4,L2,V0,M2} { sdtasdt0( sdtasdt0( skol4, skol3 )
% 48.24/48.63 , xl ) ==> xn, ! aNaturalNumber0( xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 1
% 48.24/48.63 1 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66582) {G1,W7,D4,L1,V0,M1} { sdtasdt0( sdtasdt0( skol4, skol3
% 48.24/48.63 ), xl ) ==> xn }.
% 48.24/48.63 parent0[0]: (63071) {G3,W9,D4,L2,V0,M2} P(22116,467);d(22117);r(61) { !
% 48.24/48.63 aNaturalNumber0( xl ), sdtasdt0( sdtasdt0( skol4, skol3 ), xl ) ==> xn
% 48.24/48.63 }.
% 48.24/48.63 parent1[0]: (58) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (63583) {G4,W7,D4,L1,V0,M1} S(63071);r(58) { sdtasdt0(
% 48.24/48.63 sdtasdt0( skol4, skol3 ), xl ) ==> xn }.
% 48.24/48.63 parent0: (66582) {G1,W7,D4,L1,V0,M1} { sdtasdt0( sdtasdt0( skol4, skol3 )
% 48.24/48.63 , xl ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 0 ==> 0
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 paramod: (66587) {G4,W7,D4,L1,V0,M1} { sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) ==> xn }.
% 48.24/48.63 parent0[0]: (63583) {G4,W7,D4,L1,V0,M1} S(63071);r(58) { sdtasdt0( sdtasdt0
% 48.24/48.63 ( skol4, skol3 ), xl ) ==> xn }.
% 48.24/48.63 parent1[0; 6]: (60612) {G3,W11,D4,L1,V0,M1} R(432,5543) { sdtasdt0( xl,
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) ==> sdtasdt0( sdtasdt0( skol4, skol3 ), xl )
% 48.24/48.63 }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 resolution: (66588) {G4,W0,D0,L0,V0,M0} { }.
% 48.24/48.63 parent0[0]: (9416) {G3,W7,D4,L1,V0,M1} R(67,5543) { ! sdtasdt0( xl,
% 48.24/48.63 sdtasdt0( skol4, skol3 ) ) ==> xn }.
% 48.24/48.63 parent1[0]: (66587) {G4,W7,D4,L1,V0,M1} { sdtasdt0( xl, sdtasdt0( skol4,
% 48.24/48.63 skol3 ) ) ==> xn }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 substitution1:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 subsumption: (63808) {G5,W0,D0,L0,V0,M0} S(60612);d(63583);r(9416) { }.
% 48.24/48.63 parent0: (66588) {G4,W0,D0,L0,V0,M0} { }.
% 48.24/48.63 substitution0:
% 48.24/48.63 end
% 48.24/48.63 permutation0:
% 48.24/48.63 end
% 48.24/48.63
% 48.24/48.63 Proof check complete!
% 48.24/48.63
% 48.24/48.63 Memory use:
% 48.24/48.63
% 48.24/48.63 space for terms: 934101
% 48.24/48.63 space for clauses: 3299681
% 48.24/48.63
% 48.24/48.63
% 48.24/48.63 clauses generated: 588797
% 48.24/48.63 clauses kept: 63809
% 48.24/48.63 clauses selected: 1617
% 48.24/48.63 clauses deleted: 13940
% 48.24/48.63 clauses inuse deleted: 176
% 48.24/48.63
% 48.24/48.63 subsentry: 1506441
% 48.24/48.63 literals s-matched: 731047
% 48.24/48.63 literals matched: 592197
% 48.24/48.63 full subsumption: 329391
% 48.24/48.63
% 48.24/48.63 checksum: 318868815
% 48.24/48.63
% 48.24/48.63
% 48.24/48.63 Bliksem ended
%------------------------------------------------------------------------------