%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM474+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n018.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:39 EDT 2022
% Result : Theorem 87.85s 88.30s
% Output : Refutation 87.85s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11 % Problem : NUM474+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.12 % Command : bliksem %s
% 0.12/0.32 % Computer : n018.cluster.edu
% 0.12/0.32 % Model : x86_64 x86_64
% 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32 % Memory : 8042.1875MB
% 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32 % CPULimit : 300
% 0.12/0.32 % DateTime : Thu Jul 7 02:38:53 EDT 2022
% 0.12/0.32 % CPUTime :
% 0.45/1.06 *** allocated 10000 integers for termspace/termends
% 0.45/1.06 *** allocated 10000 integers for clauses
% 0.45/1.06 *** allocated 10000 integers for justifications
% 0.45/1.06 Bliksem 1.12
% 0.45/1.06
% 0.45/1.06
% 0.45/1.06 Automatic Strategy Selection
% 0.45/1.06
% 0.45/1.06
% 0.45/1.06 Clauses:
% 0.45/1.06
% 0.45/1.06 { && }.
% 0.45/1.06 { aNaturalNumber0( sz00 ) }.
% 0.45/1.06 { aNaturalNumber0( sz10 ) }.
% 0.45/1.06 { ! sz10 = sz00 }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 0.45/1.06 ( X, Y ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 0.45/1.06 ( X, Y ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 0.45/1.06 sdtpldt0( Y, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.45/1.06 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 0.45/1.06 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 0.45/1.06 sdtasdt0( Y, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.45/1.06 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 0.45/1.06 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 0.45/1.06 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.45/1.06 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 0.45/1.06 , Z ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 0.45/1.06 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 0.45/1.06 , X ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.45/1.06 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.45/1.06 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 0.45/1.06 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.45/1.06 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 0.45/1.06 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 0.45/1.06 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.45/1.06 , X = sz00 }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 0.45/1.06 , Y = sz00 }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 0.45/1.06 , X = sz00, Y = sz00 }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.45/1.06 aNaturalNumber0( skol1( Z, T ) ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 0.45/1.06 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.45/1.06 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.45/1.06 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 0.45/1.06 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.45/1.06 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 0.45/1.06 sdtlseqdt0( Y, X ), X = Y }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 0.45/1.06 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 0.45/1.06 X }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 0.45/1.06 sdtlseqdt0( Y, X ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.45/1.06 ), ! aNaturalNumber0( Z ), alpha1( X, Y, Z ) }.
% 0.45/1.06 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 0.45/1.06 ), ! aNaturalNumber0( Z ), sdtlseqdt0( sdtpldt0( X, Z ), sdtpldt0( Y, Z
% 0.45/1.06 ) ) }.
% 0.45/1.06 { ! alpha1( X, Y, Z ), ! sdtpldt0( Z, X ) = sdtpldt0( Z, Y ) }.
% 0.45/1.06 { ! alpha1( X, Y, Z ), sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ) }.
% 0.45/1.06 { ! alpha1( X, Y, Z ), ! sdtpldt0( X, Z ) = sdtpldt0( Y, Z ) }.
% 10.78/11.22 { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), ! sdtlseqdt0( sdtpldt0( Z, X ),
% 10.78/11.22 sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) = sdtpldt0( Y, Z ), alpha1( X, Y, Z
% 10.78/11.22 ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 10.78/11.22 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), alpha2( X, Y, Z ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), X
% 10.78/11.22 = sz00, Y = Z, ! sdtlseqdt0( Y, Z ), sdtlseqdt0( sdtasdt0( Y, X ),
% 10.78/11.22 sdtasdt0( Z, X ) ) }.
% 10.78/11.22 { ! alpha2( X, Y, Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ) }.
% 10.78/11.22 { ! alpha2( X, Y, Z ), sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 10.78/11.22 { ! alpha2( X, Y, Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ) }.
% 10.78/11.22 { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), ! sdtlseqdt0( sdtasdt0( X, Y ),
% 10.78/11.22 sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) = sdtasdt0( Z, X ), alpha2( X, Y, Z
% 10.78/11.22 ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), X = sz00, X = sz10, ! sz10 = X }.
% 10.78/11.22 { ! aNaturalNumber0( X ), X = sz00, X = sz10, sdtlseqdt0( sz10, X ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, sdtlseqdt0( Y,
% 10.78/11.22 sdtasdt0( Y, X ) ) }.
% 10.78/11.22 { && }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = Y, ! sdtlseqdt0( X, Y
% 10.78/11.22 ), iLess0( X, Y ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ),
% 10.78/11.22 aNaturalNumber0( skol2( Z, T ) ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! doDivides0( X, Y ), Y =
% 10.78/11.22 sdtasdt0( X, skol2( X, Y ) ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 10.78/11.22 Y = sdtasdt0( X, Z ), doDivides0( X, Y ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 10.78/11.22 , Y ), ! Z = sdtsldt0( Y, X ), aNaturalNumber0( Z ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 10.78/11.22 , Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0( X, Z ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), X = sz00, ! doDivides0( X
% 10.78/11.22 , Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), Z = sdtsldt0( Y, X
% 10.78/11.22 ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 10.78/11.22 doDivides0( X, Y ), ! doDivides0( Y, Z ), doDivides0( X, Z ) }.
% 10.78/11.22 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 10.78/11.22 doDivides0( X, Y ), ! doDivides0( X, Z ), doDivides0( X, sdtpldt0( Y, Z
% 10.78/11.22 ) ) }.
% 10.78/11.22 { aNaturalNumber0( xl ) }.
% 10.78/11.22 { aNaturalNumber0( xm ) }.
% 10.78/11.22 { aNaturalNumber0( xn ) }.
% 10.78/11.22 { aNaturalNumber0( skol3 ) }.
% 10.78/11.22 { xm = sdtasdt0( xl, skol3 ) }.
% 10.78/11.22 { doDivides0( xl, xm ) }.
% 10.78/11.22 { aNaturalNumber0( skol5 ) }.
% 10.78/11.22 { sdtpldt0( xm, xn ) = sdtasdt0( xl, skol5 ) }.
% 10.78/11.22 { doDivides0( xl, sdtpldt0( xm, xn ) ) }.
% 10.78/11.22 { ! xl = sz00 }.
% 10.78/11.22 { aNaturalNumber0( xp ) }.
% 10.78/11.22 { xm = sdtasdt0( xl, xp ) }.
% 10.78/11.22 { xp = sdtsldt0( xm, xl ) }.
% 10.78/11.22 { aNaturalNumber0( xq ) }.
% 10.78/11.22 { sdtpldt0( xm, xn ) = sdtasdt0( xl, xq ) }.
% 10.78/11.22 { xq = sdtsldt0( sdtpldt0( xm, xn ), xl ) }.
% 10.78/11.22 { aNaturalNumber0( skol4 ) }.
% 10.78/11.22 { sdtpldt0( xp, skol4 ) = xq }.
% 10.78/11.22 { sdtlseqdt0( xp, xq ) }.
% 10.78/11.22 { aNaturalNumber0( xr ) }.
% 10.78/11.22 { sdtpldt0( xp, xr ) = xq }.
% 10.78/11.22 { xr = sdtmndt0( xq, xp ) }.
% 10.78/11.22 { ! sdtpldt0( sdtasdt0( xl, xp ), sdtasdt0( xl, xr ) ) = sdtpldt0( sdtasdt0
% 10.78/11.22 ( xl, xp ), xn ) }.
% 10.78/11.22
% 10.78/11.22 percentage equality = 0.312741, percentage horn = 0.795181
% 10.78/11.22 This is a problem with some equality
% 10.78/11.22
% 10.78/11.22
% 10.78/11.22
% 10.78/11.22 Options Used:
% 10.78/11.22
% 10.78/11.22 useres = 1
% 10.78/11.22 useparamod = 1
% 10.78/11.22 useeqrefl = 1
% 10.78/11.22 useeqfact = 1
% 10.78/11.22 usefactor = 1
% 10.78/11.22 usesimpsplitting = 0
% 10.78/11.22 usesimpdemod = 5
% 10.78/11.22 usesimpres = 3
% 10.78/11.22
% 10.78/11.22 resimpinuse = 1000
% 10.78/11.22 resimpclauses = 20000
% 10.78/11.22 substype = eqrewr
% 10.78/11.22 backwardsubs = 1
% 10.78/11.22 selectoldest = 5
% 10.78/11.22
% 10.78/11.22 litorderings [0] = split
% 10.78/11.22 litorderings [1] = extend the termordering, first sorting on arguments
% 10.78/11.22
% 10.78/11.22 termordering = kbo
% 10.78/11.22
% 10.78/11.22 litapriori = 0
% 10.78/11.22 termapriori = 1
% 10.78/11.22 litaposteriori = 0
% 10.78/11.22 termaposteriori = 0
% 10.78/11.22 demodaposteriori = 0
% 10.78/11.22 ordereqreflfact = 0
% 10.78/11.22
% 10.78/11.22 litselect = negord
% 10.78/11.22
% 10.78/11.22 maxweight = 15
% 10.78/11.22 maxdepth = 30000
% 10.78/11.22 maxlength = 115
% 10.78/11.22 maxnrvars = 195
% 10.78/11.22 excuselevel = 1
% 10.78/11.22 increasemaxweight = 1
% 10.78/11.22
% 10.78/11.22 maxselected = 10000000
% 10.78/11.22 maxnrclauses = 10000000
% 10.78/11.22
% 10.78/11.22 showgenerated = 0
% 10.78/11.22 showkept = 0
% 10.78/11.22 showselected = 0
% 10.78/11.22 showdeleted = 0
% 10.78/11.22 showresimp = 1
% 10.78/11.22 showstatus = 2000
% 10.78/11.22
% 10.78/11.22 prologoutput = 0
% 10.78/11.22 nrgoals = 5000000
% 61.66/62.07 totalproof = 1
% 61.66/62.07
% 61.66/62.07 Symbols occurring in the translation:
% 61.66/62.07
% 61.66/62.07 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 61.66/62.07 . [1, 2] (w:1, o:26, a:1, s:1, b:0),
% 61.66/62.07 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 61.66/62.07 ! [4, 1] (w:0, o:20, a:1, s:1, b:0),
% 61.66/62.07 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 61.66/62.07 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 61.66/62.07 aNaturalNumber0 [36, 1] (w:1, o:25, a:1, s:1, b:0),
% 61.66/62.07 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 61.66/62.07 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 61.66/62.07 sdtpldt0 [40, 2] (w:1, o:50, a:1, s:1, b:0),
% 61.66/62.07 sdtasdt0 [41, 2] (w:1, o:51, a:1, s:1, b:0),
% 61.66/62.07 sdtlseqdt0 [43, 2] (w:1, o:52, a:1, s:1, b:0),
% 61.66/62.07 sdtmndt0 [44, 2] (w:1, o:53, a:1, s:1, b:0),
% 61.66/62.07 iLess0 [45, 2] (w:1, o:54, a:1, s:1, b:0),
% 61.66/62.07 doDivides0 [46, 2] (w:1, o:55, a:1, s:1, b:0),
% 61.66/62.07 sdtsldt0 [47, 2] (w:1, o:56, a:1, s:1, b:0),
% 61.66/62.07 xl [48, 0] (w:1, o:11, a:1, s:1, b:0),
% 61.66/62.07 xm [49, 0] (w:1, o:12, a:1, s:1, b:0),
% 61.66/62.07 xn [50, 0] (w:1, o:13, a:1, s:1, b:0),
% 61.66/62.07 xp [51, 0] (w:1, o:14, a:1, s:1, b:0),
% 61.66/62.07 xq [52, 0] (w:1, o:15, a:1, s:1, b:0),
% 61.66/62.07 xr [53, 0] (w:1, o:16, a:1, s:1, b:0),
% 61.66/62.07 alpha1 [54, 3] (w:1, o:59, a:1, s:1, b:1),
% 61.66/62.07 alpha2 [55, 3] (w:1, o:60, a:1, s:1, b:1),
% 61.66/62.07 skol1 [56, 2] (w:1, o:57, a:1, s:1, b:1),
% 61.66/62.07 skol2 [57, 2] (w:1, o:58, a:1, s:1, b:1),
% 61.66/62.07 skol3 [58, 0] (w:1, o:17, a:1, s:1, b:1),
% 61.66/62.07 skol4 [59, 0] (w:1, o:18, a:1, s:1, b:1),
% 61.66/62.07 skol5 [60, 0] (w:1, o:19, a:1, s:1, b:1).
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Starting Search:
% 61.66/62.07
% 61.66/62.07 *** allocated 15000 integers for clauses
% 61.66/62.07 *** allocated 22500 integers for clauses
% 61.66/62.07 *** allocated 33750 integers for clauses
% 61.66/62.07 *** allocated 50625 integers for clauses
% 61.66/62.07 *** allocated 15000 integers for termspace/termends
% 61.66/62.07 *** allocated 75937 integers for clauses
% 61.66/62.07 *** allocated 22500 integers for termspace/termends
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 113905 integers for clauses
% 61.66/62.07 *** allocated 33750 integers for termspace/termends
% 61.66/62.07 *** allocated 50625 integers for termspace/termends
% 61.66/62.07 *** allocated 170857 integers for clauses
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 13039
% 61.66/62.07 Kept: 2011
% 61.66/62.07 Inuse: 130
% 61.66/62.07 Deleted: 1
% 61.66/62.07 Deletedinuse: 0
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 75937 integers for termspace/termends
% 61.66/62.07 *** allocated 256285 integers for clauses
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 113905 integers for termspace/termends
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 26247
% 61.66/62.07 Kept: 4154
% 61.66/62.07 Inuse: 179
% 61.66/62.07 Deleted: 2
% 61.66/62.07 Deletedinuse: 0
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 384427 integers for clauses
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 170857 integers for termspace/termends
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 45211
% 61.66/62.07 Kept: 6202
% 61.66/62.07 Inuse: 219
% 61.66/62.07 Deleted: 7
% 61.66/62.07 Deletedinuse: 0
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 576640 integers for clauses
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 59322
% 61.66/62.07 Kept: 8223
% 61.66/62.07 Inuse: 248
% 61.66/62.07 Deleted: 10
% 61.66/62.07 Deletedinuse: 2
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 256285 integers for termspace/termends
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 79195
% 61.66/62.07 Kept: 10239
% 61.66/62.07 Inuse: 281
% 61.66/62.07 Deleted: 18
% 61.66/62.07 Deletedinuse: 8
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 864960 integers for clauses
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 100761
% 61.66/62.07 Kept: 12362
% 61.66/62.07 Inuse: 384
% 61.66/62.07 Deleted: 44
% 61.66/62.07 Deletedinuse: 22
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 384427 integers for termspace/termends
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 131656
% 61.66/62.07 Kept: 14369
% 61.66/62.07 Inuse: 455
% 61.66/62.07 Deleted: 48
% 61.66/62.07 Deletedinuse: 22
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 150761
% 61.66/62.07 Kept: 16713
% 61.66/62.07 Inuse: 512
% 61.66/62.07 Deleted: 74
% 61.66/62.07 Deletedinuse: 25
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 *** allocated 1297440 integers for clauses
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 186523
% 61.66/62.07 Kept: 18796
% 61.66/62.07 Inuse: 560
% 61.66/62.07 Deleted: 77
% 61.66/62.07 Deletedinuse: 25
% 61.66/62.07
% 61.66/62.07 Resimplifying inuse:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07 Resimplifying clauses:
% 61.66/62.07 Done
% 61.66/62.07
% 61.66/62.07
% 61.66/62.07 Intermediate Status:
% 61.66/62.07 Generated: 208199
% 61.66/62.07 Kept: 22278
% 61.66/62.07 Inuse: 588
% 61.66/62.07 Deleted: 5911
% 87.85/88.30 Deletedinuse: 26
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 576640 integers for termspace/termends
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 232286
% 87.85/88.30 Kept: 24337
% 87.85/88.30 Inuse: 639
% 87.85/88.30 Deleted: 6065
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 259654
% 87.85/88.30 Kept: 26585
% 87.85/88.30 Inuse: 682
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 1946160 integers for clauses
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 273093
% 87.85/88.30 Kept: 28668
% 87.85/88.30 Inuse: 712
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 284608
% 87.85/88.30 Kept: 30698
% 87.85/88.30 Inuse: 736
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 299883
% 87.85/88.30 Kept: 32841
% 87.85/88.30 Inuse: 772
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 310531
% 87.85/88.30 Kept: 35442
% 87.85/88.30 Inuse: 792
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 316835
% 87.85/88.30 Kept: 37494
% 87.85/88.30 Inuse: 802
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 864960 integers for termspace/termends
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 2919240 integers for clauses
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 325810
% 87.85/88.30 Kept: 39517
% 87.85/88.30 Inuse: 820
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 334786
% 87.85/88.30 Kept: 41609
% 87.85/88.30 Inuse: 838
% 87.85/88.30 Deleted: 6067
% 87.85/88.30 Deletedinuse: 178
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying clauses:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 344496
% 87.85/88.30 Kept: 43609
% 87.85/88.30 Inuse: 852
% 87.85/88.30 Deleted: 13061
% 87.85/88.30 Deletedinuse: 180
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 358419
% 87.85/88.30 Kept: 45733
% 87.85/88.30 Inuse: 882
% 87.85/88.30 Deleted: 13061
% 87.85/88.30 Deletedinuse: 180
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 376660
% 87.85/88.30 Kept: 47760
% 87.85/88.30 Inuse: 922
% 87.85/88.30 Deleted: 13061
% 87.85/88.30 Deletedinuse: 180
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 398858
% 87.85/88.30 Kept: 49792
% 87.85/88.30 Inuse: 967
% 87.85/88.30 Deleted: 13141
% 87.85/88.30 Deletedinuse: 254
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 430867
% 87.85/88.30 Kept: 51802
% 87.85/88.30 Inuse: 1036
% 87.85/88.30 Deleted: 13150
% 87.85/88.30 Deletedinuse: 258
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 457154
% 87.85/88.30 Kept: 53807
% 87.85/88.30 Inuse: 1108
% 87.85/88.30 Deleted: 13150
% 87.85/88.30 Deletedinuse: 258
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 483996
% 87.85/88.30 Kept: 55845
% 87.85/88.30 Inuse: 1155
% 87.85/88.30 Deleted: 13154
% 87.85/88.30 Deletedinuse: 262
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 4378860 integers for clauses
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 509321
% 87.85/88.30 Kept: 57867
% 87.85/88.30 Inuse: 1228
% 87.85/88.30 Deleted: 13155
% 87.85/88.30 Deletedinuse: 263
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 1297440 integers for termspace/termends
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 534683
% 87.85/88.30 Kept: 59888
% 87.85/88.30 Inuse: 1281
% 87.85/88.30 Deleted: 13163
% 87.85/88.30 Deletedinuse: 271
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 556131
% 87.85/88.30 Kept: 61904
% 87.85/88.30 Inuse: 1328
% 87.85/88.30 Deleted: 13205
% 87.85/88.30 Deletedinuse: 313
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying clauses:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 592366
% 87.85/88.30 Kept: 65611
% 87.85/88.30 Inuse: 1391
% 87.85/88.30 Deleted: 25947
% 87.85/88.30 Deletedinuse: 319
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 608861
% 87.85/88.30 Kept: 67625
% 87.85/88.30 Inuse: 1433
% 87.85/88.30 Deleted: 25951
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 632003
% 87.85/88.30 Kept: 69633
% 87.85/88.30 Inuse: 1484
% 87.85/88.30 Deleted: 25951
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 656385
% 87.85/88.30 Kept: 71716
% 87.85/88.30 Inuse: 1545
% 87.85/88.30 Deleted: 25952
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 676966
% 87.85/88.30 Kept: 73802
% 87.85/88.30 Inuse: 1621
% 87.85/88.30 Deleted: 25952
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 708144
% 87.85/88.30 Kept: 75830
% 87.85/88.30 Inuse: 1675
% 87.85/88.30 Deleted: 25958
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 746926
% 87.85/88.30 Kept: 77831
% 87.85/88.30 Inuse: 1779
% 87.85/88.30 Deleted: 25959
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 845886
% 87.85/88.30 Kept: 80936
% 87.85/88.30 Inuse: 2038
% 87.85/88.30 Deleted: 25959
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 861590
% 87.85/88.30 Kept: 82950
% 87.85/88.30 Inuse: 2048
% 87.85/88.30 Deleted: 25959
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 *** allocated 6568290 integers for clauses
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Intermediate Status:
% 87.85/88.30 Generated: 883556
% 87.85/88.30 Kept: 85265
% 87.85/88.30 Inuse: 2063
% 87.85/88.30 Deleted: 25959
% 87.85/88.30 Deletedinuse: 323
% 87.85/88.30
% 87.85/88.30 Resimplifying inuse:
% 87.85/88.30 Done
% 87.85/88.30
% 87.85/88.30 Resimplifying clauses:
% 87.85/88.30
% 87.85/88.30 Bliksems!, er is een bewijs:
% 87.85/88.30 % SZS status Theorem
% 87.85/88.30 % SZS output start Refutation
% 87.85/88.30
% 87.85/88.30 (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 87.85/88.30 , aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 87.85/88.30 (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 87.85/88.30 , aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 87.85/88.30 (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 87.85/88.30 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.30 (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 87.85/88.30 ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.85/88.30 (16) {G0,W19,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 87.85/88.30 ), ! aNaturalNumber0( Z ), sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z )
% 87.85/88.30 ) ==> sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 87.85/88.30 (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.85/88.30 (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 87.85/88.30 (62) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 87.85/88.30 (70) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 87.85/88.30 (71) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, xp ) ==> xm }.
% 87.85/88.30 (73) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xq ) }.
% 87.85/88.30 (74) {G0,W7,D3,L1,V0,M1} I { sdtasdt0( xl, xq ) ==> sdtpldt0( xm, xn ) }.
% 87.85/88.30 (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.85/88.30 (80) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xq }.
% 87.85/88.30 (82) {G1,W9,D4,L1,V0,M1} I;d(71) { ! sdtpldt0( xm, sdtasdt0( xl, xr ) ) ==>
% 87.85/88.30 sdtpldt0( xm, xn ) }.
% 87.85/88.30 (238) {G1,W6,D3,L2,V1,M2} R(4,79) { ! aNaturalNumber0( X ), aNaturalNumber0
% 87.85/88.30 ( sdtpldt0( xr, X ) ) }.
% 87.85/88.30 (251) {G1,W6,D3,L2,V1,M2} R(5,60) { ! aNaturalNumber0( X ), aNaturalNumber0
% 87.85/88.30 ( sdtasdt0( xl, X ) ) }.
% 87.85/88.30 (293) {G1,W9,D3,L2,V1,M2} R(6,61) { ! aNaturalNumber0( X ), sdtpldt0( xm, X
% 87.85/88.30 ) = sdtpldt0( X, xm ) }.
% 87.85/88.30 (308) {G1,W7,D3,L2,V0,M2} P(80,6);r(70) { ! aNaturalNumber0( xr ), sdtpldt0
% 87.85/88.30 ( xr, xp ) ==> xq }.
% 87.85/88.30 (413) {G1,W9,D3,L2,V1,M2} R(10,60) { ! aNaturalNumber0( X ), sdtasdt0( xl,
% 87.85/88.30 X ) = sdtasdt0( X, xl ) }.
% 87.85/88.30 (580) {G1,W17,D4,L3,V2,M3} R(16,79) { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) ) ==>
% 87.85/88.30 sdtasdt0( X, sdtpldt0( xr, Y ) ) }.
% 87.85/88.30 (5792) {G2,W4,D3,L1,V0,M1} R(251,79) { aNaturalNumber0( sdtasdt0( xl, xr )
% 87.85/88.30 ) }.
% 87.85/88.30 (10480) {G1,W9,D3,L2,V0,M2} P(74,10);r(60) { ! aNaturalNumber0( xq ),
% 87.85/88.30 sdtasdt0( xq, xl ) ==> sdtpldt0( xm, xn ) }.
% 87.85/88.30 (21665) {G2,W7,D3,L1,V0,M1} S(10480);r(73) { sdtasdt0( xq, xl ) ==>
% 87.85/88.30 sdtpldt0( xm, xn ) }.
% 87.85/88.30 (22264) {G2,W5,D3,L1,V0,M1} S(308);r(79) { sdtpldt0( xr, xp ) ==> xq }.
% 87.85/88.30 (48520) {G2,W7,D3,L1,V0,M1} R(293,62) { sdtpldt0( xm, xn ) ==> sdtpldt0( xn
% 87.85/88.30 , xm ) }.
% 87.85/88.30 (48536) {G3,W9,D4,L1,V0,M1} P(293,82);d(48520);r(5792) { ! sdtpldt0(
% 87.85/88.30 sdtasdt0( xl, xr ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.85/88.30 (60118) {G2,W13,D4,L2,V1,M2} R(413,238) { sdtasdt0( xl, sdtpldt0( xr, X ) )
% 87.85/88.30 ==> sdtasdt0( sdtpldt0( xr, X ), xl ), ! aNaturalNumber0( X ) }.
% 87.85/88.30 (60209) {G2,W7,D3,L1,V0,M1} R(413,79) { sdtasdt0( xl, xr ) ==> sdtasdt0( xr
% 87.85/88.30 , xl ) }.
% 87.85/88.30 (64931) {G4,W9,D4,L1,V0,M1} S(48536);d(60209) { ! sdtpldt0( sdtasdt0( xr,
% 87.85/88.30 xl ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.85/88.30 (65492) {G3,W7,D3,L1,V0,M1} S(21665);d(48520) { sdtasdt0( xq, xl ) ==>
% 87.85/88.30 sdtpldt0( xn, xm ) }.
% 87.85/88.30 (77638) {G4,W11,D4,L2,V0,M2} P(71,580);d(60209);d(60118);d(22264);d(65492);
% 87.85/88.30 r(60) { ! aNaturalNumber0( xp ), sdtpldt0( sdtasdt0( xr, xl ), xm ) ==>
% 87.85/88.30 sdtpldt0( xn, xm ) }.
% 87.85/88.30 (87525) {G5,W0,D0,L0,V0,M0} S(77638);r(70);r(64931) { }.
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 % SZS output end Refutation
% 87.85/88.30 found a proof!
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Unprocessed initial clauses:
% 87.85/88.30
% 87.85/88.30 (87527) {G0,W1,D1,L1,V0,M1} { && }.
% 87.85/88.30 (87528) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 87.85/88.30 (87529) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 87.85/88.30 (87530) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 87.85/88.30 (87531) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 87.85/88.30 ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 87.85/88.30 (87532) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 87.85/88.30 ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 87.85/88.30 (87533) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.30 (87534) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0(
% 87.85/88.30 X, sdtpldt0( Y, Z ) ) }.
% 87.85/88.30 (87535) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 87.85/88.30 = X }.
% 87.85/88.30 (87536) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00,
% 87.85/88.30 X ) }.
% 87.85/88.30 (87537) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.85/88.30 (87538) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0(
% 87.85/88.30 X, sdtasdt0( Y, Z ) ) }.
% 87.85/88.30 (87539) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 87.85/88.30 = X }.
% 87.85/88.30 (87540) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10,
% 87.85/88.30 X ) }.
% 87.85/88.30 (87541) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 87.85/88.30 = sz00 }.
% 87.85/88.30 (87542) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 87.85/88.30 sz00, X ) }.
% 87.85/88.30 (87543) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0(
% 87.85/88.30 sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 87.85/88.30 (87544) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0(
% 87.85/88.30 sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 87.85/88.30 (87545) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 87.85/88.30 }.
% 87.85/88.30 (87546) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z
% 87.85/88.30 }.
% 87.85/88.30 (87547) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 87.85/88.30 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 87.85/88.30 sdtasdt0( X, Z ), Y = Z }.
% 87.85/88.30 (87548) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 87.85/88.30 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 87.85/88.30 sdtasdt0( Z, X ), Y = Z }.
% 87.85/88.30 (87549) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 87.85/88.30 (87550) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 87.85/88.30 (87551) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 87.85/88.30 (87552) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 87.85/88.30 (87553) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 87.85/88.30 (87554) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 87.85/88.30 }.
% 87.85/88.30 (87555) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 87.85/88.30 }.
% 87.85/88.30 (87556) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 87.85/88.30 }.
% 87.85/88.30 (87557) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y
% 87.85/88.30 , Z = sdtmndt0( Y, X ) }.
% 87.85/88.30 (87558) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 87.85/88.30 }.
% 87.85/88.30 (87559) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 87.85/88.30 (87560) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ),
% 87.85/88.30 sdtlseqdt0( X, Z ) }.
% 87.85/88.30 (87561) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 87.85/88.30 (87562) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 87.85/88.30 (87563) {G0,W16,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), alpha1( X, Y, Z
% 87.85/88.30 ) }.
% 87.85/88.30 (87564) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = Y, ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), sdtlseqdt0(
% 87.85/88.30 sdtpldt0( X, Z ), sdtpldt0( Y, Z ) ) }.
% 87.85/88.30 (87565) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), ! sdtpldt0( Z, X ) =
% 87.85/88.30 sdtpldt0( Z, Y ) }.
% 87.85/88.30 (87566) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), sdtlseqdt0( sdtpldt0(
% 87.85/88.30 Z, X ), sdtpldt0( Z, Y ) ) }.
% 87.85/88.30 (87567) {G0,W11,D3,L2,V3,M2} { ! alpha1( X, Y, Z ), ! sdtpldt0( X, Z ) =
% 87.85/88.30 sdtpldt0( Y, Z ) }.
% 87.85/88.30 (87568) {G0,W25,D3,L4,V3,M4} { sdtpldt0( Z, X ) = sdtpldt0( Z, Y ), !
% 87.85/88.30 sdtlseqdt0( sdtpldt0( Z, X ), sdtpldt0( Z, Y ) ), sdtpldt0( X, Z ) =
% 87.85/88.30 sdtpldt0( Y, Z ), alpha1( X, Y, Z ) }.
% 87.85/88.30 (87569) {G0,W19,D2,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 87.85/88.30 alpha2( X, Y, Z ) }.
% 87.85/88.30 (87570) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), X = sz00, Y = Z, ! sdtlseqdt0( Y, Z ),
% 87.85/88.30 sdtlseqdt0( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 87.85/88.30 (87571) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), ! sdtasdt0( X, Y ) =
% 87.85/88.30 sdtasdt0( X, Z ) }.
% 87.85/88.30 (87572) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), sdtlseqdt0( sdtasdt0(
% 87.85/88.30 X, Y ), sdtasdt0( X, Z ) ) }.
% 87.85/88.30 (87573) {G0,W11,D3,L2,V3,M2} { ! alpha2( X, Y, Z ), ! sdtasdt0( Y, X ) =
% 87.85/88.30 sdtasdt0( Z, X ) }.
% 87.85/88.30 (87574) {G0,W25,D3,L4,V3,M4} { sdtasdt0( X, Y ) = sdtasdt0( X, Z ), !
% 87.85/88.30 sdtlseqdt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), sdtasdt0( Y, X ) =
% 87.85/88.30 sdtasdt0( Z, X ), alpha2( X, Y, Z ) }.
% 87.85/88.30 (87575) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 87.85/88.30 , ! sz10 = X }.
% 87.85/88.30 (87576) {G0,W11,D2,L4,V1,M4} { ! aNaturalNumber0( X ), X = sz00, X = sz10
% 87.85/88.30 , sdtlseqdt0( sz10, X ) }.
% 87.85/88.30 (87577) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = sz00, sdtlseqdt0( Y, sdtasdt0( Y, X ) ) }.
% 87.85/88.30 (87578) {G0,W1,D1,L1,V0,M1} { && }.
% 87.85/88.30 (87579) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = Y, ! sdtlseqdt0( X, Y ), iLess0( X, Y ) }.
% 87.85/88.30 (87580) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! doDivides0( X, Y ), aNaturalNumber0( skol2( Z, T ) ) }.
% 87.85/88.30 (87581) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! doDivides0( X, Y ), Y = sdtasdt0( X, skol2( X, Y ) ) }.
% 87.85/88.30 (87582) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! Y = sdtasdt0( X, Z ), doDivides0( X, Y )
% 87.85/88.30 }.
% 87.85/88.30 (87583) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ),
% 87.85/88.30 aNaturalNumber0( Z ) }.
% 87.85/88.30 (87584) {G0,W20,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = sz00, ! doDivides0( X, Y ), ! Z = sdtsldt0( Y, X ), Y = sdtasdt0
% 87.85/88.30 ( X, Z ) }.
% 87.85/88.30 (87585) {G0,W22,D3,L7,V3,M7} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), X = sz00, ! doDivides0( X, Y ), ! aNaturalNumber0( Z ), ! Y =
% 87.85/88.30 sdtasdt0( X, Z ), Z = sdtsldt0( Y, X ) }.
% 87.85/88.30 (87586) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( Y, Z ),
% 87.85/88.30 doDivides0( X, Z ) }.
% 87.85/88.30 (87587) {G0,W17,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 87.85/88.30 Y ), ! aNaturalNumber0( Z ), ! doDivides0( X, Y ), ! doDivides0( X, Z ),
% 87.85/88.30 doDivides0( X, sdtpldt0( Y, Z ) ) }.
% 87.85/88.30 (87588) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 87.85/88.30 (87589) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 87.85/88.30 (87590) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 87.85/88.30 (87591) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol3 ) }.
% 87.85/88.30 (87592) {G0,W5,D3,L1,V0,M1} { xm = sdtasdt0( xl, skol3 ) }.
% 87.85/88.30 (87593) {G0,W3,D2,L1,V0,M1} { doDivides0( xl, xm ) }.
% 87.85/88.30 (87594) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol5 ) }.
% 87.85/88.30 (87595) {G0,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) = sdtasdt0( xl, skol5 )
% 87.85/88.30 }.
% 87.85/88.30 (87596) {G0,W5,D3,L1,V0,M1} { doDivides0( xl, sdtpldt0( xm, xn ) ) }.
% 87.85/88.30 (87597) {G0,W3,D2,L1,V0,M1} { ! xl = sz00 }.
% 87.85/88.30 (87598) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 87.85/88.30 (87599) {G0,W5,D3,L1,V0,M1} { xm = sdtasdt0( xl, xp ) }.
% 87.85/88.30 (87600) {G0,W5,D3,L1,V0,M1} { xp = sdtsldt0( xm, xl ) }.
% 87.85/88.30 (87601) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xq ) }.
% 87.85/88.30 (87602) {G0,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) = sdtasdt0( xl, xq ) }.
% 87.85/88.30 (87603) {G0,W7,D4,L1,V0,M1} { xq = sdtsldt0( sdtpldt0( xm, xn ), xl ) }.
% 87.85/88.30 (87604) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol4 ) }.
% 87.85/88.30 (87605) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, skol4 ) = xq }.
% 87.85/88.30 (87606) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xp, xq ) }.
% 87.85/88.30 (87607) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xr ) }.
% 87.85/88.30 (87608) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, xr ) = xq }.
% 87.85/88.30 (87609) {G0,W5,D3,L1,V0,M1} { xr = sdtmndt0( xq, xp ) }.
% 87.85/88.30 (87610) {G0,W13,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl, xp ), sdtasdt0(
% 87.85/88.30 xl, xr ) ) = sdtpldt0( sdtasdt0( xl, xp ), xn ) }.
% 87.85/88.30
% 87.85/88.30
% 87.85/88.30 Total Proof:
% 87.85/88.30
% 87.85/88.30 subsumption: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 87.85/88.30 parent0: (87531) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 87.85/88.30 substitution0:
% 87.85/88.30 X := X
% 87.85/88.30 Y := Y
% 87.85/88.30 end
% 87.85/88.30 permutation0:
% 87.85/88.30 0 ==> 0
% 87.85/88.30 1 ==> 1
% 87.85/88.30 2 ==> 2
% 87.85/88.30 end
% 87.85/88.30
% 87.85/88.30 subsumption: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 87.85/88.30 parent0: (87532) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 87.85/88.30 substitution0:
% 87.85/88.30 X := X
% 87.85/88.30 Y := Y
% 87.85/88.30 end
% 87.85/88.30 permutation0:
% 87.85/88.30 0 ==> 0
% 87.85/88.30 1 ==> 1
% 87.85/88.30 2 ==> 2
% 87.85/88.30 end
% 87.85/88.30
% 87.85/88.30 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.30 parent0: (87533) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.30 substitution0:
% 87.85/88.30 X := X
% 87.85/88.30 Y := Y
% 87.85/88.30 end
% 87.85/88.30 permutation0:
% 87.85/88.30 0 ==> 0
% 87.85/88.30 1 ==> 1
% 87.85/88.30 2 ==> 2
% 87.85/88.30 end
% 87.85/88.30
% 87.85/88.30 subsumption: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.85/88.30 parent0: (87537) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.85/88.30 substitution0:
% 87.85/88.30 X := X
% 87.85/88.30 Y := Y
% 87.85/88.30 end
% 87.85/88.30 permutation0:
% 87.85/88.30 0 ==> 0
% 87.85/88.30 1 ==> 1
% 87.85/88.30 2 ==> 2
% 87.85/88.30 end
% 87.85/88.30
% 87.85/88.30 eqswap: (87665) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Y ),
% 87.85/88.30 sdtasdt0( X, Z ) ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aNaturalNumber0(
% 87.85/88.30 X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 87.85/88.30 parent0[3]: (87543) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z
% 87.85/88.30 ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 87.85/88.30 substitution0:
% 87.85/88.30 X := X
% 87.85/88.30 Y := Y
% 87.85/88.30 Z := Z
% 87.85/88.30 end
% 87.85/88.30
% 87.85/88.30 subsumption: (16) {G0,W19,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), !
% 87.85/88.30 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtasdt0( X, Y )
% 87.85/88.30 , sdtasdt0( X, Z ) ) ==> sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 87.85/88.30 parent0: (87665) {G0,W19,D4,L4,V3,M4} { sdtpldt0( sdtasdt0( X, Y ),
% 87.85/88.32 sdtasdt0( X, Z ) ) = sdtasdt0( X, sdtpldt0( Y, Z ) ), ! aNaturalNumber0(
% 87.85/88.32 X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 Y := Y
% 87.85/88.32 Z := Z
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 3
% 87.85/88.32 1 ==> 0
% 87.85/88.32 2 ==> 1
% 87.85/88.32 3 ==> 2
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.85/88.32 parent0: (87588) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 87.85/88.32 parent0: (87589) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 *** allocated 1946160 integers for termspace/termends
% 87.85/88.32 subsumption: (62) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 87.85/88.32 parent0: (87590) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (70) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 87.85/88.32 parent0: (87598) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xp ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 eqswap: (89550) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xl, xp ) = xm }.
% 87.85/88.32 parent0[0]: (87599) {G0,W5,D3,L1,V0,M1} { xm = sdtasdt0( xl, xp ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (71) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, xp ) ==> xm }.
% 87.85/88.32 parent0: (89550) {G0,W5,D3,L1,V0,M1} { sdtasdt0( xl, xp ) = xm }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (73) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xq ) }.
% 87.85/88.32 parent0: (87601) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xq ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 eqswap: (90309) {G0,W7,D3,L1,V0,M1} { sdtasdt0( xl, xq ) = sdtpldt0( xm,
% 87.85/88.32 xn ) }.
% 87.85/88.32 parent0[0]: (87602) {G0,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) = sdtasdt0(
% 87.85/88.32 xl, xq ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (74) {G0,W7,D3,L1,V0,M1} I { sdtasdt0( xl, xq ) ==> sdtpldt0(
% 87.85/88.32 xm, xn ) }.
% 87.85/88.32 parent0: (90309) {G0,W7,D3,L1,V0,M1} { sdtasdt0( xl, xq ) = sdtpldt0( xm,
% 87.85/88.32 xn ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.85/88.32 parent0: (87607) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xr ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (80) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xq }.
% 87.85/88.32 parent0: (87608) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xp, xr ) = xq }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 paramod: (91552) {G1,W11,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl, xp ),
% 87.85/88.32 sdtasdt0( xl, xr ) ) = sdtpldt0( xm, xn ) }.
% 87.85/88.32 parent0[0]: (71) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, xp ) ==> xm }.
% 87.85/88.32 parent1[0; 10]: (87610) {G0,W13,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl,
% 87.85/88.32 xp ), sdtasdt0( xl, xr ) ) = sdtpldt0( sdtasdt0( xl, xp ), xn ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 paramod: (91553) {G1,W9,D4,L1,V0,M1} { ! sdtpldt0( xm, sdtasdt0( xl, xr )
% 87.85/88.32 ) = sdtpldt0( xm, xn ) }.
% 87.85/88.32 parent0[0]: (71) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, xp ) ==> xm }.
% 87.85/88.32 parent1[0; 3]: (91552) {G1,W11,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl, xp
% 87.85/88.32 ), sdtasdt0( xl, xr ) ) = sdtpldt0( xm, xn ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (82) {G1,W9,D4,L1,V0,M1} I;d(71) { ! sdtpldt0( xm, sdtasdt0(
% 87.85/88.32 xl, xr ) ) ==> sdtpldt0( xm, xn ) }.
% 87.85/88.32 parent0: (91553) {G1,W9,D4,L1,V0,M1} { ! sdtpldt0( xm, sdtasdt0( xl, xr )
% 87.85/88.32 ) = sdtpldt0( xm, xn ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91557) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtpldt0( xr, X ) ) }.
% 87.85/88.32 parent0[0]: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 87.85/88.32 parent1[0]: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := xr
% 87.85/88.32 Y := X
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (238) {G1,W6,D3,L2,V1,M2} R(4,79) { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtpldt0( xr, X ) ) }.
% 87.85/88.32 parent0: (91557) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtpldt0( xr, X ) ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 1 ==> 1
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91559) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtasdt0( xl, X ) ) }.
% 87.85/88.32 parent0[0]: (5) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 87.85/88.32 parent1[0]: (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := xl
% 87.85/88.32 Y := X
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (251) {G1,W6,D3,L2,V1,M2} R(5,60) { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtasdt0( xl, X ) ) }.
% 87.85/88.32 parent0: (91559) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 87.85/88.32 aNaturalNumber0( sdtasdt0( xl, X ) ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 1 ==> 1
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91561) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0
% 87.85/88.32 ( xm, X ) = sdtpldt0( X, xm ) }.
% 87.85/88.32 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.32 parent1[0]: (61) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := xm
% 87.85/88.32 Y := X
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (293) {G1,W9,D3,L2,V1,M2} R(6,61) { ! aNaturalNumber0( X ),
% 87.85/88.32 sdtpldt0( xm, X ) = sdtpldt0( X, xm ) }.
% 87.85/88.32 parent0: (91561) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0(
% 87.85/88.32 xm, X ) = sdtpldt0( X, xm ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 1 ==> 1
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 eqswap: (91563) {G0,W5,D3,L1,V0,M1} { xq ==> sdtpldt0( xp, xr ) }.
% 87.85/88.32 parent0[0]: (80) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xp, xr ) ==> xq }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 paramod: (91564) {G1,W9,D3,L3,V0,M3} { xq ==> sdtpldt0( xr, xp ), !
% 87.85/88.32 aNaturalNumber0( xp ), ! aNaturalNumber0( xr ) }.
% 87.85/88.32 parent0[2]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 87.85/88.32 parent1[0; 2]: (91563) {G0,W5,D3,L1,V0,M1} { xq ==> sdtpldt0( xp, xr ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := xp
% 87.85/88.32 Y := xr
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91604) {G1,W7,D3,L2,V0,M2} { xq ==> sdtpldt0( xr, xp ), !
% 87.85/88.32 aNaturalNumber0( xr ) }.
% 87.85/88.32 parent0[1]: (91564) {G1,W9,D3,L3,V0,M3} { xq ==> sdtpldt0( xr, xp ), !
% 87.85/88.32 aNaturalNumber0( xp ), ! aNaturalNumber0( xr ) }.
% 87.85/88.32 parent1[0]: (70) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 eqswap: (91605) {G1,W7,D3,L2,V0,M2} { sdtpldt0( xr, xp ) ==> xq, !
% 87.85/88.32 aNaturalNumber0( xr ) }.
% 87.85/88.32 parent0[0]: (91604) {G1,W7,D3,L2,V0,M2} { xq ==> sdtpldt0( xr, xp ), !
% 87.85/88.32 aNaturalNumber0( xr ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (308) {G1,W7,D3,L2,V0,M2} P(80,6);r(70) { ! aNaturalNumber0(
% 87.85/88.32 xr ), sdtpldt0( xr, xp ) ==> xq }.
% 87.85/88.32 parent0: (91605) {G1,W7,D3,L2,V0,M2} { sdtpldt0( xr, xp ) ==> xq, !
% 87.85/88.32 aNaturalNumber0( xr ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 1
% 87.85/88.32 1 ==> 0
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91606) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0
% 87.85/88.32 ( xl, X ) = sdtasdt0( X, xl ) }.
% 87.85/88.32 parent0[0]: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.85/88.32 parent1[0]: (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := xl
% 87.85/88.32 Y := X
% 87.85/88.32 end
% 87.85/88.32 substitution1:
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 subsumption: (413) {G1,W9,D3,L2,V1,M2} R(10,60) { ! aNaturalNumber0( X ),
% 87.85/88.32 sdtasdt0( xl, X ) = sdtasdt0( X, xl ) }.
% 87.85/88.32 parent0: (91606) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0(
% 87.85/88.32 xl, X ) = sdtasdt0( X, xl ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 end
% 87.85/88.32 permutation0:
% 87.85/88.32 0 ==> 0
% 87.85/88.32 1 ==> 1
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 eqswap: (91608) {G0,W19,D4,L4,V3,M4} { sdtasdt0( X, sdtpldt0( Y, Z ) ) ==>
% 87.85/88.32 sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), ! aNaturalNumber0( X ),
% 87.85/88.32 ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 87.85/88.32 parent0[3]: (16) {G0,W19,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), !
% 87.85/88.32 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtasdt0( X, Y )
% 87.85/88.32 , sdtasdt0( X, Z ) ) ==> sdtasdt0( X, sdtpldt0( Y, Z ) ) }.
% 87.85/88.32 substitution0:
% 87.85/88.32 X := X
% 87.85/88.32 Y := Y
% 87.85/88.32 Z := Z
% 87.85/88.32 end
% 87.85/88.32
% 87.85/88.32 resolution: (91610) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( xr, Y )
% 87.85/88.32 ) ==> sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) ), ! aNaturalNumber0
% 87.85/88.32 ( X ), ! aNaturalNumber0( Y ) }.
% 87.85/88.32 parent0[2]: (91608) {G0,W19,D4,L4,V3,M4} { sdtasdt0( X, sdtpldt0( Y, Z ) )
% 87.85/88.32 ==> sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ), ! aNaturalNumber0( X
% 87.85/88.32 ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 87.93/88.32 parent1[0]: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 Y := xr
% 87.93/88.32 Z := Y
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91613) {G1,W17,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, xr ),
% 87.93/88.32 sdtasdt0( X, Y ) ) ==> sdtasdt0( X, sdtpldt0( xr, Y ) ), !
% 87.93/88.32 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 87.93/88.32 parent0[0]: (91610) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( xr, Y )
% 87.93/88.32 ) ==> sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) ), ! aNaturalNumber0
% 87.93/88.32 ( X ), ! aNaturalNumber0( Y ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 Y := Y
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (580) {G1,W17,D4,L3,V2,M3} R(16,79) { ! aNaturalNumber0( X ),
% 87.93/88.32 ! aNaturalNumber0( Y ), sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) )
% 87.93/88.32 ==> sdtasdt0( X, sdtpldt0( xr, Y ) ) }.
% 87.93/88.32 parent0: (91613) {G1,W17,D4,L3,V2,M3} { sdtpldt0( sdtasdt0( X, xr ),
% 87.93/88.32 sdtasdt0( X, Y ) ) ==> sdtasdt0( X, sdtpldt0( xr, Y ) ), !
% 87.93/88.32 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 Y := Y
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 2
% 87.93/88.32 1 ==> 0
% 87.93/88.32 2 ==> 1
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91621) {G1,W4,D3,L1,V0,M1} { aNaturalNumber0( sdtasdt0( xl,
% 87.93/88.32 xr ) ) }.
% 87.93/88.32 parent0[0]: (251) {G1,W6,D3,L2,V1,M2} R(5,60) { ! aNaturalNumber0( X ),
% 87.93/88.32 aNaturalNumber0( sdtasdt0( xl, X ) ) }.
% 87.93/88.32 parent1[0]: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := xr
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (5792) {G2,W4,D3,L1,V0,M1} R(251,79) { aNaturalNumber0(
% 87.93/88.32 sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 parent0: (91621) {G1,W4,D3,L1,V0,M1} { aNaturalNumber0( sdtasdt0( xl, xr )
% 87.93/88.32 ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91622) {G0,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) ==> sdtasdt0( xl
% 87.93/88.32 , xq ) }.
% 87.93/88.32 parent0[0]: (74) {G0,W7,D3,L1,V0,M1} I { sdtasdt0( xl, xq ) ==> sdtpldt0(
% 87.93/88.32 xm, xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91623) {G1,W11,D3,L3,V0,M3} { sdtpldt0( xm, xn ) ==> sdtasdt0(
% 87.93/88.32 xq, xl ), ! aNaturalNumber0( xl ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 parent0[2]: (10) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 87.93/88.32 aNaturalNumber0( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 87.93/88.32 parent1[0; 4]: (91622) {G0,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtasdt0( xl, xq ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := xl
% 87.93/88.32 Y := xq
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91663) {G1,W9,D3,L2,V0,M2} { sdtpldt0( xm, xn ) ==> sdtasdt0
% 87.93/88.32 ( xq, xl ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 parent0[1]: (91623) {G1,W11,D3,L3,V0,M3} { sdtpldt0( xm, xn ) ==> sdtasdt0
% 87.93/88.32 ( xq, xl ), ! aNaturalNumber0( xl ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 parent1[0]: (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91664) {G1,W9,D3,L2,V0,M2} { sdtasdt0( xq, xl ) ==> sdtpldt0( xm
% 87.93/88.32 , xn ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 parent0[0]: (91663) {G1,W9,D3,L2,V0,M2} { sdtpldt0( xm, xn ) ==> sdtasdt0
% 87.93/88.32 ( xq, xl ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (10480) {G1,W9,D3,L2,V0,M2} P(74,10);r(60) { ! aNaturalNumber0
% 87.93/88.32 ( xq ), sdtasdt0( xq, xl ) ==> sdtpldt0( xm, xn ) }.
% 87.93/88.32 parent0: (91664) {G1,W9,D3,L2,V0,M2} { sdtasdt0( xq, xl ) ==> sdtpldt0( xm
% 87.93/88.32 , xn ), ! aNaturalNumber0( xq ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 1
% 87.93/88.32 1 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91666) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xq, xl ) ==> sdtpldt0
% 87.93/88.32 ( xm, xn ) }.
% 87.93/88.32 parent0[0]: (10480) {G1,W9,D3,L2,V0,M2} P(74,10);r(60) { ! aNaturalNumber0
% 87.93/88.32 ( xq ), sdtasdt0( xq, xl ) ==> sdtpldt0( xm, xn ) }.
% 87.93/88.32 parent1[0]: (73) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xq ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (21665) {G2,W7,D3,L1,V0,M1} S(10480);r(73) { sdtasdt0( xq, xl
% 87.93/88.32 ) ==> sdtpldt0( xm, xn ) }.
% 87.93/88.32 parent0: (91666) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xq, xl ) ==> sdtpldt0( xm
% 87.93/88.32 , xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91669) {G1,W5,D3,L1,V0,M1} { sdtpldt0( xr, xp ) ==> xq }.
% 87.93/88.32 parent0[0]: (308) {G1,W7,D3,L2,V0,M2} P(80,6);r(70) { ! aNaturalNumber0( xr
% 87.93/88.32 ), sdtpldt0( xr, xp ) ==> xq }.
% 87.93/88.32 parent1[0]: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (22264) {G2,W5,D3,L1,V0,M1} S(308);r(79) { sdtpldt0( xr, xp )
% 87.93/88.32 ==> xq }.
% 87.93/88.32 parent0: (91669) {G1,W5,D3,L1,V0,M1} { sdtpldt0( xr, xp ) ==> xq }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91671) {G1,W9,D3,L2,V1,M2} { sdtpldt0( X, xm ) = sdtpldt0( xm, X
% 87.93/88.32 ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent0[1]: (293) {G1,W9,D3,L2,V1,M2} R(6,61) { ! aNaturalNumber0( X ),
% 87.93/88.32 sdtpldt0( xm, X ) = sdtpldt0( X, xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91672) {G1,W7,D3,L1,V0,M1} { sdtpldt0( xn, xm ) = sdtpldt0(
% 87.93/88.32 xm, xn ) }.
% 87.93/88.32 parent0[1]: (91671) {G1,W9,D3,L2,V1,M2} { sdtpldt0( X, xm ) = sdtpldt0( xm
% 87.93/88.32 , X ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent1[0]: (62) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := xn
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91673) {G1,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) = sdtpldt0( xn,
% 87.93/88.32 xm ) }.
% 87.93/88.32 parent0[0]: (91672) {G1,W7,D3,L1,V0,M1} { sdtpldt0( xn, xm ) = sdtpldt0(
% 87.93/88.32 xm, xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (48520) {G2,W7,D3,L1,V0,M1} R(293,62) { sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0: (91673) {G1,W7,D3,L1,V0,M1} { sdtpldt0( xm, xn ) = sdtpldt0( xn,
% 87.93/88.32 xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91675) {G1,W9,D4,L1,V0,M1} { ! sdtpldt0( xm, xn ) ==> sdtpldt0(
% 87.93/88.32 xm, sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 parent0[0]: (82) {G1,W9,D4,L1,V0,M1} I;d(71) { ! sdtpldt0( xm, sdtasdt0( xl
% 87.93/88.32 , xr ) ) ==> sdtpldt0( xm, xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91678) {G2,W13,D4,L2,V0,M2} { ! sdtpldt0( xm, xn ) ==> sdtpldt0
% 87.93/88.32 ( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 parent0[1]: (293) {G1,W9,D3,L2,V1,M2} R(6,61) { ! aNaturalNumber0( X ),
% 87.93/88.32 sdtpldt0( xm, X ) = sdtpldt0( X, xm ) }.
% 87.93/88.32 parent1[0; 5]: (91675) {G1,W9,D4,L1,V0,M1} { ! sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtpldt0( xm, sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := sdtasdt0( xl, xr )
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91680) {G3,W13,D4,L2,V0,M2} { ! sdtpldt0( xn, xm ) ==> sdtpldt0
% 87.93/88.32 ( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 parent0[0]: (48520) {G2,W7,D3,L1,V0,M1} R(293,62) { sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent1[0; 2]: (91678) {G2,W13,D4,L2,V0,M2} { ! sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( sdtasdt0( xl, xr )
% 87.93/88.32 ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91681) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( xn, xm ) ==>
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ) }.
% 87.93/88.32 parent0[1]: (91680) {G3,W13,D4,L2,V0,M2} { ! sdtpldt0( xn, xm ) ==>
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( sdtasdt0( xl, xr )
% 87.93/88.32 ) }.
% 87.93/88.32 parent1[0]: (5792) {G2,W4,D3,L1,V0,M1} R(251,79) { aNaturalNumber0(
% 87.93/88.32 sdtasdt0( xl, xr ) ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91682) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl, xr ), xm )
% 87.93/88.32 ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0[0]: (91681) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( xn, xm ) ==>
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (48536) {G3,W9,D4,L1,V0,M1} P(293,82);d(48520);r(5792) { !
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0: (91682) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xl, xr ), xm
% 87.93/88.32 ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91683) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl, X
% 87.93/88.32 ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent0[1]: (413) {G1,W9,D3,L2,V1,M2} R(10,60) { ! aNaturalNumber0( X ),
% 87.93/88.32 sdtasdt0( xl, X ) = sdtasdt0( X, xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91684) {G2,W13,D4,L2,V1,M2} { sdtasdt0( sdtpldt0( xr, X ), xl
% 87.93/88.32 ) = sdtasdt0( xl, sdtpldt0( xr, X ) ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent0[1]: (91683) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl
% 87.93/88.32 , X ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent1[1]: (238) {G1,W6,D3,L2,V1,M2} R(4,79) { ! aNaturalNumber0( X ),
% 87.93/88.32 aNaturalNumber0( sdtpldt0( xr, X ) ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := sdtpldt0( xr, X )
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91685) {G2,W13,D4,L2,V1,M2} { sdtasdt0( xl, sdtpldt0( xr, X ) ) =
% 87.93/88.32 sdtasdt0( sdtpldt0( xr, X ), xl ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent0[0]: (91684) {G2,W13,D4,L2,V1,M2} { sdtasdt0( sdtpldt0( xr, X ), xl
% 87.93/88.32 ) = sdtasdt0( xl, sdtpldt0( xr, X ) ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (60118) {G2,W13,D4,L2,V1,M2} R(413,238) { sdtasdt0( xl,
% 87.93/88.32 sdtpldt0( xr, X ) ) ==> sdtasdt0( sdtpldt0( xr, X ), xl ), !
% 87.93/88.32 aNaturalNumber0( X ) }.
% 87.93/88.32 parent0: (91685) {G2,W13,D4,L2,V1,M2} { sdtasdt0( xl, sdtpldt0( xr, X ) )
% 87.93/88.32 = sdtasdt0( sdtpldt0( xr, X ), xl ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 1 ==> 1
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91686) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl, X
% 87.93/88.32 ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent0[1]: (413) {G1,W9,D3,L2,V1,M2} R(10,60) { ! aNaturalNumber0( X ),
% 87.93/88.32 sdtasdt0( xl, X ) = sdtasdt0( X, xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91687) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xr, xl ) = sdtasdt0(
% 87.93/88.32 xl, xr ) }.
% 87.93/88.32 parent0[1]: (91686) {G1,W9,D3,L2,V1,M2} { sdtasdt0( X, xl ) = sdtasdt0( xl
% 87.93/88.32 , X ), ! aNaturalNumber0( X ) }.
% 87.93/88.32 parent1[0]: (79) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xr ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := xr
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91688) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xl, xr ) = sdtasdt0( xr,
% 87.93/88.32 xl ) }.
% 87.93/88.32 parent0[0]: (91687) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xr, xl ) = sdtasdt0(
% 87.93/88.32 xl, xr ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (60209) {G2,W7,D3,L1,V0,M1} R(413,79) { sdtasdt0( xl, xr ) ==>
% 87.93/88.32 sdtasdt0( xr, xl ) }.
% 87.93/88.32 parent0: (91688) {G1,W7,D3,L1,V0,M1} { sdtasdt0( xl, xr ) = sdtasdt0( xr,
% 87.93/88.32 xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91691) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xr, xl ), xm
% 87.93/88.32 ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0[0]: (60209) {G2,W7,D3,L1,V0,M1} R(413,79) { sdtasdt0( xl, xr ) ==>
% 87.93/88.32 sdtasdt0( xr, xl ) }.
% 87.93/88.32 parent1[0; 3]: (48536) {G3,W9,D4,L1,V0,M1} P(293,82);d(48520);r(5792) { !
% 87.93/88.32 sdtpldt0( sdtasdt0( xl, xr ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (64931) {G4,W9,D4,L1,V0,M1} S(48536);d(60209) { ! sdtpldt0(
% 87.93/88.32 sdtasdt0( xr, xl ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0: (91691) {G3,W9,D4,L1,V0,M1} { ! sdtpldt0( sdtasdt0( xr, xl ), xm
% 87.93/88.32 ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91695) {G3,W7,D3,L1,V0,M1} { sdtasdt0( xq, xl ) ==> sdtpldt0( xn
% 87.93/88.32 , xm ) }.
% 87.93/88.32 parent0[0]: (48520) {G2,W7,D3,L1,V0,M1} R(293,62) { sdtpldt0( xm, xn ) ==>
% 87.93/88.32 sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent1[0; 4]: (21665) {G2,W7,D3,L1,V0,M1} S(10480);r(73) { sdtasdt0( xq,
% 87.93/88.32 xl ) ==> sdtpldt0( xm, xn ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (65492) {G3,W7,D3,L1,V0,M1} S(21665);d(48520) { sdtasdt0( xq,
% 87.93/88.32 xl ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0: (91695) {G3,W7,D3,L1,V0,M1} { sdtasdt0( xq, xl ) ==> sdtpldt0( xn
% 87.93/88.32 , xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91698) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( xr, Y ) )
% 87.93/88.32 ==> sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) ), ! aNaturalNumber0( X
% 87.93/88.32 ), ! aNaturalNumber0( Y ) }.
% 87.93/88.32 parent0[2]: (580) {G1,W17,D4,L3,V2,M3} R(16,79) { ! aNaturalNumber0( X ), !
% 87.93/88.32 aNaturalNumber0( Y ), sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) )
% 87.93/88.32 ==> sdtasdt0( X, sdtpldt0( xr, Y ) ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := X
% 87.93/88.32 Y := Y
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91703) {G1,W15,D4,L3,V0,M3} { sdtasdt0( xl, sdtpldt0( xr, xp ) )
% 87.93/88.32 ==> sdtpldt0( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( xl ), !
% 87.93/88.32 aNaturalNumber0( xp ) }.
% 87.93/88.32 parent0[0]: (71) {G0,W5,D3,L1,V0,M1} I { sdtasdt0( xl, xp ) ==> xm }.
% 87.93/88.32 parent1[0; 10]: (91698) {G1,W17,D4,L3,V2,M3} { sdtasdt0( X, sdtpldt0( xr,
% 87.93/88.32 Y ) ) ==> sdtpldt0( sdtasdt0( X, xr ), sdtasdt0( X, Y ) ), !
% 87.93/88.32 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 X := xl
% 87.93/88.32 Y := xp
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91704) {G2,W15,D4,L3,V0,M3} { sdtasdt0( xl, sdtpldt0( xr, xp ) )
% 87.93/88.32 ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xl ), !
% 87.93/88.32 aNaturalNumber0( xp ) }.
% 87.93/88.32 parent0[0]: (60209) {G2,W7,D3,L1,V0,M1} R(413,79) { sdtasdt0( xl, xr ) ==>
% 87.93/88.32 sdtasdt0( xr, xl ) }.
% 87.93/88.32 parent1[0; 7]: (91703) {G1,W15,D4,L3,V0,M3} { sdtasdt0( xl, sdtpldt0( xr,
% 87.93/88.32 xp ) ) ==> sdtpldt0( sdtasdt0( xl, xr ), xm ), ! aNaturalNumber0( xl ), !
% 87.93/88.32 aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91705) {G3,W17,D4,L4,V0,M4} { sdtasdt0( sdtpldt0( xr, xp ), xl )
% 87.93/88.32 ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), !
% 87.93/88.32 aNaturalNumber0( xl ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 parent0[0]: (60118) {G2,W13,D4,L2,V1,M2} R(413,238) { sdtasdt0( xl,
% 87.93/88.32 sdtpldt0( xr, X ) ) ==> sdtasdt0( sdtpldt0( xr, X ), xl ), !
% 87.93/88.32 aNaturalNumber0( X ) }.
% 87.93/88.32 parent1[0; 1]: (91704) {G2,W15,D4,L3,V0,M3} { sdtasdt0( xl, sdtpldt0( xr,
% 87.93/88.32 xp ) ) ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xl ), !
% 87.93/88.32 aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 X := xp
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 factor: (91706) {G3,W15,D4,L3,V0,M3} { sdtasdt0( sdtpldt0( xr, xp ), xl )
% 87.93/88.32 ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), !
% 87.93/88.32 aNaturalNumber0( xl ) }.
% 87.93/88.32 parent0[1, 3]: (91705) {G3,W17,D4,L4,V0,M4} { sdtasdt0( sdtpldt0( xr, xp )
% 87.93/88.32 , xl ) ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), !
% 87.93/88.32 aNaturalNumber0( xl ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91707) {G3,W13,D4,L3,V0,M3} { sdtasdt0( xq, xl ) ==> sdtpldt0(
% 87.93/88.32 sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( xl
% 87.93/88.32 ) }.
% 87.93/88.32 parent0[0]: (22264) {G2,W5,D3,L1,V0,M1} S(308);r(79) { sdtpldt0( xr, xp )
% 87.93/88.32 ==> xq }.
% 87.93/88.32 parent1[0; 2]: (91706) {G3,W15,D4,L3,V0,M3} { sdtasdt0( sdtpldt0( xr, xp )
% 87.93/88.32 , xl ) ==> sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), !
% 87.93/88.32 aNaturalNumber0( xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 paramod: (91708) {G4,W13,D4,L3,V0,M3} { sdtpldt0( xn, xm ) ==> sdtpldt0(
% 87.93/88.32 sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), ! aNaturalNumber0( xl
% 87.93/88.32 ) }.
% 87.93/88.32 parent0[0]: (65492) {G3,W7,D3,L1,V0,M1} S(21665);d(48520) { sdtasdt0( xq,
% 87.93/88.32 xl ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent1[0; 1]: (91707) {G3,W13,D4,L3,V0,M3} { sdtasdt0( xq, xl ) ==>
% 87.93/88.32 sdtpldt0( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), !
% 87.93/88.32 aNaturalNumber0( xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91709) {G1,W11,D4,L2,V0,M2} { sdtpldt0( xn, xm ) ==> sdtpldt0
% 87.93/88.32 ( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 parent0[2]: (91708) {G4,W13,D4,L3,V0,M3} { sdtpldt0( xn, xm ) ==> sdtpldt0
% 87.93/88.32 ( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ), ! aNaturalNumber0(
% 87.93/88.32 xl ) }.
% 87.93/88.32 parent1[0]: (60) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 eqswap: (91710) {G1,W11,D4,L2,V0,M2} { sdtpldt0( sdtasdt0( xr, xl ), xm )
% 87.93/88.32 ==> sdtpldt0( xn, xm ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 parent0[0]: (91709) {G1,W11,D4,L2,V0,M2} { sdtpldt0( xn, xm ) ==> sdtpldt0
% 87.93/88.32 ( sdtasdt0( xr, xl ), xm ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (77638) {G4,W11,D4,L2,V0,M2} P(71,580);d(60209);d(60118);d(
% 87.93/88.32 22264);d(65492);r(60) { ! aNaturalNumber0( xp ), sdtpldt0( sdtasdt0( xr,
% 87.93/88.32 xl ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0: (91710) {G1,W11,D4,L2,V0,M2} { sdtpldt0( sdtasdt0( xr, xl ), xm )
% 87.93/88.32 ==> sdtpldt0( xn, xm ), ! aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 0 ==> 1
% 87.93/88.32 1 ==> 0
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91713) {G1,W9,D4,L1,V0,M1} { sdtpldt0( sdtasdt0( xr, xl ), xm
% 87.93/88.32 ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent0[0]: (77638) {G4,W11,D4,L2,V0,M2} P(71,580);d(60209);d(60118);d(
% 87.93/88.32 22264);d(65492);r(60) { ! aNaturalNumber0( xp ), sdtpldt0( sdtasdt0( xr,
% 87.93/88.32 xl ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent1[0]: (70) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xp ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 resolution: (91714) {G2,W0,D0,L0,V0,M0} { }.
% 87.93/88.32 parent0[0]: (64931) {G4,W9,D4,L1,V0,M1} S(48536);d(60209) { ! sdtpldt0(
% 87.93/88.32 sdtasdt0( xr, xl ), xm ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 parent1[0]: (91713) {G1,W9,D4,L1,V0,M1} { sdtpldt0( sdtasdt0( xr, xl ), xm
% 87.93/88.32 ) ==> sdtpldt0( xn, xm ) }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 substitution1:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 subsumption: (87525) {G5,W0,D0,L0,V0,M0} S(77638);r(70);r(64931) { }.
% 87.93/88.32 parent0: (91714) {G2,W0,D0,L0,V0,M0} { }.
% 87.93/88.32 substitution0:
% 87.93/88.32 end
% 87.93/88.32 permutation0:
% 87.93/88.32 end
% 87.93/88.32
% 87.93/88.32 Proof check complete!
% 87.93/88.32
% 87.93/88.32 Memory use:
% 87.93/88.32
% 87.93/88.32 space for terms: 1277071
% 87.93/88.32 space for clauses: 4522242
% 87.93/88.32
% 87.93/88.32
% 87.93/88.32 clauses generated: 894719
% 87.93/88.32 clauses kept: 87526
% 87.93/88.32 clauses selected: 2068
% 87.93/88.32 clauses deleted: 27427
% 87.93/88.32 clauses inuse deleted: 323
% 87.93/88.32
% 87.93/88.32 subsentry: 2630924
% 87.93/88.32 literals s-matched: 1198859
% 87.93/88.32 literals matched: 961478
% 87.93/88.32 full subsumption: 506031
% 87.93/88.32
% 87.93/88.32 checksum: 373643452
% 87.93/88.32
% 87.93/88.32
% 87.93/88.32 Bliksem ended
%------------------------------------------------------------------------------