%------------------------------------------------------------------------------
% File : Bliksem---1.12
% Problem : NUM461+2 : TPTP v8.1.0. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : bliksem %s
% Computer : n012.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:30 EDT 2022
% Result : Theorem 226.47s 226.91s
% Output : Refutation 226.47s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NUM461+2 : TPTP v8.1.0. Released v4.0.0.
% 0.03/0.13 % Command : bliksem %s
% 0.14/0.34 % Computer : n012.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % DateTime : Tue Jul 5 18:49:15 EDT 2022
% 0.14/0.34 % CPUTime :
% 3.32/3.71 *** allocated 10000 integers for termspace/termends
% 3.32/3.71 *** allocated 10000 integers for clauses
% 3.32/3.71 *** allocated 10000 integers for justifications
% 3.32/3.71 Bliksem 1.12
% 3.32/3.71
% 3.32/3.71
% 3.32/3.71 Automatic Strategy Selection
% 3.32/3.71
% 3.32/3.71
% 3.32/3.71 Clauses:
% 3.32/3.71
% 3.32/3.71 { && }.
% 3.32/3.71 { aNaturalNumber0( sz00 ) }.
% 3.32/3.71 { aNaturalNumber0( sz10 ) }.
% 3.32/3.71 { ! sz10 = sz00 }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0
% 3.32/3.71 ( X, Y ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), aNaturalNumber0( sdtasdt0
% 3.32/3.71 ( X, Y ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtpldt0( X, Y ) =
% 3.32/3.71 sdtpldt0( Y, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 3.32/3.71 sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 ) = X }.
% 3.32/3.71 { ! aNaturalNumber0( X ), X = sdtpldt0( sz00, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtasdt0( X, Y ) =
% 3.32/3.71 sdtasdt0( Y, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 3.32/3.71 sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0( X, sdtasdt0( Y, Z ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 ) = X }.
% 3.32/3.71 { ! aNaturalNumber0( X ), X = sdtasdt0( sz10, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 ) = sz00 }.
% 3.32/3.71 { ! aNaturalNumber0( X ), sz00 = sdtasdt0( sz00, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 3.32/3.71 sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0( sdtasdt0( X, Y ), sdtasdt0( X
% 3.32/3.71 , Z ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ),
% 3.32/3.71 sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0( sdtasdt0( Y, X ), sdtasdt0( Z
% 3.32/3.71 , X ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 3.32/3.71 sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 3.32/3.71 sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y = Z }.
% 3.32/3.71 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 3.32/3.71 aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) = sdtasdt0( X, Z ), Y = Z }.
% 3.32/3.71 { ! aNaturalNumber0( X ), X = sz00, ! aNaturalNumber0( Y ), !
% 3.32/3.71 aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) = sdtasdt0( Z, X ), Y = Z }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 3.32/3.71 , X = sz00 }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtpldt0( X, Y ) = sz00
% 3.32/3.71 , Y = sz00 }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtasdt0( X, Y ) = sz00
% 3.32/3.71 , X = sz00, Y = sz00 }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 3.32/3.71 aNaturalNumber0( skol1( Z, T ) ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ),
% 3.32/3.71 sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 3.32/3.71 sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 3.32/3.71 = sdtmndt0( Y, X ), aNaturalNumber0( Z ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), ! Z
% 3.32/3.71 = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 3.32/3.71 aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, Z = sdtmndt0( Y, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), sdtlseqdt0( X, X ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! sdtlseqdt0( X, Y ), !
% 3.32/3.71 sdtlseqdt0( Y, X ), X = Y }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), !
% 3.32/3.71 sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z ), sdtlseqdt0( X, Z ) }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ), ! Y =
% 3.32/3.71 X }.
% 3.32/3.71 { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y ), sdtlseqdt0( X, Y ),
% 3.32/3.71 sdtlseqdt0( Y, X ) }.
% 3.32/3.71 { aNaturalNumber0( xl ) }.
% 3.32/3.71 { aNaturalNumber0( xn ) }.
% 3.32/3.71 { ! xl = xn }.
% 3.32/3.71 { aNaturalNumber0( skol2 ) }.
% 3.32/3.71 { sdtpldt0( xl, skol2 ) = xn }.
% 3.32/3.71 { sdtlseqdt0( xl, xn ) }.
% 3.32/3.71 { aNaturalNumber0( xm ) }.
% 3.32/3.71 { sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ), alpha1, sdtpldt0( xl, xm ) =
% 3.32/3.71 sdtpldt0( xn, xm ), ! aNaturalNumber0( X ), ! sdtpldt0( sdtpldt0( xl, xm
% 3.32/3.71 ), X ) = sdtpldt0( xn, xm ) }.
% 3.32/3.71 { sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ), alpha1, sdtpldt0( xl, xm ) =
% 3.32/3.71 sdtpldt0( xn, xm ), ! sdtlseqdt0( sdtpldt0( xl, xm ), sdtpldt0( xn, xm )
% 51.12/51.50 ) }.
% 51.12/51.50 { ! alpha1, ! aNaturalNumber0( X ), ! sdtpldt0( sdtpldt0( xm, xl ), X ) =
% 51.12/51.50 sdtpldt0( xm, xn ) }.
% 51.12/51.50 { ! alpha1, ! sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ) }.
% 51.12/51.50 { aNaturalNumber0( skol3 ), sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm,
% 51.12/51.50 xn ) ), alpha1 }.
% 51.12/51.50 { sdtpldt0( sdtpldt0( xm, xl ), skol3 ) = sdtpldt0( xm, xn ), sdtlseqdt0(
% 51.12/51.50 sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 51.12/51.50
% 51.12/51.50 percentage equality = 0.307692, percentage horn = 0.836735
% 51.12/51.50 This is a problem with some equality
% 51.12/51.50
% 51.12/51.50
% 51.12/51.50
% 51.12/51.50 Options Used:
% 51.12/51.50
% 51.12/51.50 useres = 1
% 51.12/51.50 useparamod = 1
% 51.12/51.50 useeqrefl = 1
% 51.12/51.50 useeqfact = 1
% 51.12/51.50 usefactor = 1
% 51.12/51.50 usesimpsplitting = 0
% 51.12/51.50 usesimpdemod = 5
% 51.12/51.50 usesimpres = 3
% 51.12/51.50
% 51.12/51.50 resimpinuse = 1000
% 51.12/51.50 resimpclauses = 20000
% 51.12/51.50 substype = eqrewr
% 51.12/51.50 backwardsubs = 1
% 51.12/51.50 selectoldest = 5
% 51.12/51.50
% 51.12/51.50 litorderings [0] = split
% 51.12/51.50 litorderings [1] = extend the termordering, first sorting on arguments
% 51.12/51.50
% 51.12/51.50 termordering = kbo
% 51.12/51.50
% 51.12/51.50 litapriori = 0
% 51.12/51.50 termapriori = 1
% 51.12/51.50 litaposteriori = 0
% 51.12/51.50 termaposteriori = 0
% 51.12/51.50 demodaposteriori = 0
% 51.12/51.50 ordereqreflfact = 0
% 51.12/51.50
% 51.12/51.50 litselect = negord
% 51.12/51.50
% 51.12/51.50 maxweight = 15
% 51.12/51.50 maxdepth = 30000
% 51.12/51.50 maxlength = 115
% 51.12/51.50 maxnrvars = 195
% 51.12/51.50 excuselevel = 1
% 51.12/51.50 increasemaxweight = 1
% 51.12/51.50
% 51.12/51.50 maxselected = 10000000
% 51.12/51.50 maxnrclauses = 10000000
% 51.12/51.50
% 51.12/51.50 showgenerated = 0
% 51.12/51.50 showkept = 0
% 51.12/51.50 showselected = 0
% 51.12/51.50 showdeleted = 0
% 51.12/51.50 showresimp = 1
% 51.12/51.50 showstatus = 2000
% 51.12/51.50
% 51.12/51.50 prologoutput = 0
% 51.12/51.50 nrgoals = 5000000
% 51.12/51.50 totalproof = 1
% 51.12/51.50
% 51.12/51.50 Symbols occurring in the translation:
% 51.12/51.50
% 51.12/51.50 {} [0, 0] (w:1, o:2, a:1, s:1, b:0),
% 51.12/51.50 . [1, 2] (w:1, o:23, a:1, s:1, b:0),
% 51.12/51.50 && [3, 0] (w:1, o:4, a:1, s:1, b:0),
% 51.12/51.50 ! [4, 1] (w:0, o:17, a:1, s:1, b:0),
% 51.12/51.50 = [13, 2] (w:1, o:0, a:0, s:1, b:0),
% 51.12/51.50 ==> [14, 2] (w:1, o:0, a:0, s:1, b:0),
% 51.12/51.50 aNaturalNumber0 [36, 1] (w:1, o:22, a:1, s:1, b:0),
% 51.12/51.50 sz00 [37, 0] (w:1, o:7, a:1, s:1, b:0),
% 51.12/51.50 sz10 [38, 0] (w:1, o:8, a:1, s:1, b:0),
% 51.12/51.50 sdtpldt0 [40, 2] (w:1, o:47, a:1, s:1, b:0),
% 51.12/51.50 sdtasdt0 [41, 2] (w:1, o:48, a:1, s:1, b:0),
% 51.12/51.50 sdtlseqdt0 [43, 2] (w:1, o:49, a:1, s:1, b:0),
% 51.12/51.50 sdtmndt0 [44, 2] (w:1, o:50, a:1, s:1, b:0),
% 51.12/51.50 xl [45, 0] (w:1, o:11, a:1, s:1, b:0),
% 51.12/51.50 xn [46, 0] (w:1, o:13, a:1, s:1, b:0),
% 51.12/51.50 xm [47, 0] (w:1, o:12, a:1, s:1, b:0),
% 51.12/51.50 alpha1 [48, 0] (w:1, o:14, a:1, s:1, b:1),
% 51.12/51.50 skol1 [49, 2] (w:1, o:51, a:1, s:1, b:1),
% 51.12/51.50 skol2 [50, 0] (w:1, o:15, a:1, s:1, b:1),
% 51.12/51.50 skol3 [51, 0] (w:1, o:16, a:1, s:1, b:1).
% 51.12/51.50
% 51.12/51.50
% 51.12/51.50 Starting Search:
% 51.12/51.50
% 51.12/51.50 *** allocated 15000 integers for clauses
% 51.12/51.50 *** allocated 22500 integers for clauses
% 51.12/51.50 *** allocated 33750 integers for clauses
% 51.12/51.50 *** allocated 50625 integers for clauses
% 51.12/51.50 *** allocated 75937 integers for clauses
% 51.12/51.50 *** allocated 15000 integers for termspace/termends
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 22500 integers for termspace/termends
% 51.12/51.50 *** allocated 113905 integers for clauses
% 51.12/51.50 *** allocated 33750 integers for termspace/termends
% 51.12/51.50 *** allocated 170857 integers for clauses
% 51.12/51.50
% 51.12/51.50 Intermediate Status:
% 51.12/51.50 Generated: 12089
% 51.12/51.50 Kept: 2003
% 51.12/51.50 Inuse: 113
% 51.12/51.50 Deleted: 6
% 51.12/51.50 Deletedinuse: 5
% 51.12/51.50
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 50625 integers for termspace/termends
% 51.12/51.50 *** allocated 256285 integers for clauses
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 75937 integers for termspace/termends
% 51.12/51.50
% 51.12/51.50 Intermediate Status:
% 51.12/51.50 Generated: 24143
% 51.12/51.50 Kept: 4014
% 51.12/51.50 Inuse: 173
% 51.12/51.50 Deleted: 14
% 51.12/51.50 Deletedinuse: 10
% 51.12/51.50
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 113905 integers for termspace/termends
% 51.12/51.50 *** allocated 384427 integers for clauses
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50
% 51.12/51.50 Intermediate Status:
% 51.12/51.50 Generated: 34451
% 51.12/51.50 Kept: 6105
% 51.12/51.50 Inuse: 244
% 51.12/51.50 Deleted: 25
% 51.12/51.50 Deletedinuse: 11
% 51.12/51.50
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 576640 integers for clauses
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 170857 integers for termspace/termends
% 51.12/51.50
% 51.12/51.50 Intermediate Status:
% 51.12/51.50 Generated: 53644
% 51.12/51.50 Kept: 8127
% 51.12/51.50 Inuse: 301
% 51.12/51.50 Deleted: 29
% 51.12/51.50 Deletedinuse: 11
% 51.12/51.50
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 Resimplifying inuse:
% 51.12/51.50 Done
% 51.12/51.50
% 51.12/51.50 *** allocated 864960 integers for clauses
% 51.12/51.50
% 51.12/51.50 Intermediate Status:
% 173.89/174.31 Generated: 72849
% 173.89/174.31 Kept: 10159
% 173.89/174.31 Inuse: 352
% 173.89/174.31 Deleted: 32
% 173.89/174.31 Deletedinuse: 12
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 89470
% 173.89/174.31 Kept: 12178
% 173.89/174.31 Inuse: 402
% 173.89/174.31 Deleted: 40
% 173.89/174.31 Deletedinuse: 14
% 173.89/174.31
% 173.89/174.31 *** allocated 256285 integers for termspace/termends
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 96174
% 173.89/174.31 Kept: 14212
% 173.89/174.31 Inuse: 416
% 173.89/174.31 Deleted: 42
% 173.89/174.31 Deletedinuse: 16
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 *** allocated 1297440 integers for clauses
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 106445
% 173.89/174.31 Kept: 16980
% 173.89/174.31 Inuse: 440
% 173.89/174.31 Deleted: 42
% 173.89/174.31 Deletedinuse: 16
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 111823
% 173.89/174.31 Kept: 19114
% 173.89/174.31 Inuse: 450
% 173.89/174.31 Deleted: 42
% 173.89/174.31 Deletedinuse: 16
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 *** allocated 384427 integers for termspace/termends
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying clauses:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 116344
% 173.89/174.31 Kept: 21326
% 173.89/174.31 Inuse: 455
% 173.89/174.31 Deleted: 1568
% 173.89/174.31 Deletedinuse: 16
% 173.89/174.31
% 173.89/174.31 *** allocated 1946160 integers for clauses
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 120170
% 173.89/174.31 Kept: 23380
% 173.89/174.31 Inuse: 461
% 173.89/174.31 Deleted: 1581
% 173.89/174.31 Deletedinuse: 29
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 126726
% 173.89/174.31 Kept: 25476
% 173.89/174.31 Inuse: 480
% 173.89/174.31 Deleted: 1581
% 173.89/174.31 Deletedinuse: 29
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 143601
% 173.89/174.31 Kept: 27580
% 173.89/174.31 Inuse: 532
% 173.89/174.31 Deleted: 1598
% 173.89/174.31 Deletedinuse: 45
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 *** allocated 576640 integers for termspace/termends
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 158507
% 173.89/174.31 Kept: 29598
% 173.89/174.31 Inuse: 573
% 173.89/174.31 Deleted: 1677
% 173.89/174.31 Deletedinuse: 121
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 176057
% 173.89/174.31 Kept: 31658
% 173.89/174.31 Inuse: 621
% 173.89/174.31 Deleted: 1723
% 173.89/174.31 Deletedinuse: 158
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 186480
% 173.89/174.31 Kept: 33699
% 173.89/174.31 Inuse: 643
% 173.89/174.31 Deleted: 1724
% 173.89/174.31 Deletedinuse: 158
% 173.89/174.31
% 173.89/174.31 *** allocated 2919240 integers for clauses
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 193661
% 173.89/174.31 Kept: 35750
% 173.89/174.31 Inuse: 656
% 173.89/174.31 Deleted: 1724
% 173.89/174.31 Deletedinuse: 158
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 211334
% 173.89/174.31 Kept: 37757
% 173.89/174.31 Inuse: 683
% 173.89/174.31 Deleted: 1767
% 173.89/174.31 Deletedinuse: 158
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 232011
% 173.89/174.31 Kept: 39775
% 173.89/174.31 Inuse: 717
% 173.89/174.31 Deleted: 1799
% 173.89/174.31 Deletedinuse: 158
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying clauses:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 254638
% 173.89/174.31 Kept: 42275
% 173.89/174.31 Inuse: 739
% 173.89/174.31 Deleted: 13686
% 173.89/174.31 Deletedinuse: 162
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 *** allocated 864960 integers for termspace/termends
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 271489
% 173.89/174.31 Kept: 44358
% 173.89/174.31 Inuse: 781
% 173.89/174.31 Deleted: 13713
% 173.89/174.31 Deletedinuse: 188
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 286476
% 173.89/174.31 Kept: 46385
% 173.89/174.31 Inuse: 809
% 173.89/174.31 Deleted: 13719
% 173.89/174.31 Deletedinuse: 193
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 295641
% 173.89/174.31 Kept: 48436
% 173.89/174.31 Inuse: 825
% 173.89/174.31 Deleted: 13720
% 173.89/174.31 Deletedinuse: 193
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 *** allocated 4378860 integers for clauses
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 307435
% 173.89/174.31 Kept: 50680
% 173.89/174.31 Inuse: 845
% 173.89/174.31 Deleted: 13720
% 173.89/174.31 Deletedinuse: 193
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 317550
% 173.89/174.31 Kept: 52731
% 173.89/174.31 Inuse: 863
% 173.89/174.31 Deleted: 13720
% 173.89/174.31 Deletedinuse: 193
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 327938
% 173.89/174.31 Kept: 54914
% 173.89/174.31 Inuse: 880
% 173.89/174.31 Deleted: 13720
% 173.89/174.31 Deletedinuse: 193
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31 Resimplifying inuse:
% 173.89/174.31 Done
% 173.89/174.31
% 173.89/174.31
% 173.89/174.31 Intermediate Status:
% 173.89/174.31 Generated: 337148
% 173.89/174.31 Kept: 56984
% 226.47/226.91 Inuse: 896
% 226.47/226.91 Deleted: 13720
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 349691
% 226.47/226.91 Kept: 59059
% 226.47/226.91 Inuse: 921
% 226.47/226.91 Deleted: 13720
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 362466
% 226.47/226.91 Kept: 61136
% 226.47/226.91 Inuse: 944
% 226.47/226.91 Deleted: 13720
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying clauses:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 373508
% 226.47/226.91 Kept: 63186
% 226.47/226.91 Inuse: 958
% 226.47/226.91 Deleted: 16172
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 381827
% 226.47/226.91 Kept: 65216
% 226.47/226.91 Inuse: 972
% 226.47/226.91 Deleted: 16172
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 *** allocated 1297440 integers for termspace/termends
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 394220
% 226.47/226.91 Kept: 67230
% 226.47/226.91 Inuse: 996
% 226.47/226.91 Deleted: 16172
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 407180
% 226.47/226.91 Kept: 69244
% 226.47/226.91 Inuse: 1018
% 226.47/226.91 Deleted: 16172
% 226.47/226.91 Deletedinuse: 193
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 424163
% 226.47/226.91 Kept: 71290
% 226.47/226.91 Inuse: 1041
% 226.47/226.91 Deleted: 16182
% 226.47/226.91 Deletedinuse: 200
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 433018
% 226.47/226.91 Kept: 73526
% 226.47/226.91 Inuse: 1054
% 226.47/226.91 Deleted: 16324
% 226.47/226.91 Deletedinuse: 339
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 *** allocated 6568290 integers for clauses
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 461428
% 226.47/226.91 Kept: 75849
% 226.47/226.91 Inuse: 1086
% 226.47/226.91 Deleted: 16393
% 226.47/226.91 Deletedinuse: 365
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 493452
% 226.47/226.91 Kept: 77928
% 226.47/226.91 Inuse: 1160
% 226.47/226.91 Deleted: 16404
% 226.47/226.91 Deletedinuse: 366
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 505326
% 226.47/226.91 Kept: 79954
% 226.47/226.91 Inuse: 1177
% 226.47/226.91 Deleted: 16410
% 226.47/226.91 Deletedinuse: 372
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 515732
% 226.47/226.91 Kept: 82067
% 226.47/226.91 Inuse: 1192
% 226.47/226.91 Deleted: 16413
% 226.47/226.91 Deletedinuse: 375
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying clauses:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 543749
% 226.47/226.91 Kept: 88738
% 226.47/226.91 Inuse: 1199
% 226.47/226.91 Deleted: 40748
% 226.47/226.91 Deletedinuse: 375
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 553549
% 226.47/226.91 Kept: 90756
% 226.47/226.91 Inuse: 1216
% 226.47/226.91 Deleted: 40757
% 226.47/226.91 Deletedinuse: 384
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 564668
% 226.47/226.91 Kept: 92791
% 226.47/226.91 Inuse: 1242
% 226.47/226.91 Deleted: 40763
% 226.47/226.91 Deletedinuse: 389
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 575359
% 226.47/226.91 Kept: 95251
% 226.47/226.91 Inuse: 1260
% 226.47/226.91 Deleted: 40763
% 226.47/226.91 Deletedinuse: 389
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 583169
% 226.47/226.91 Kept: 97606
% 226.47/226.91 Inuse: 1275
% 226.47/226.91 Deleted: 40763
% 226.47/226.91 Deletedinuse: 389
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 590519
% 226.47/226.91 Kept: 99639
% 226.47/226.91 Inuse: 1287
% 226.47/226.91 Deleted: 40763
% 226.47/226.91 Deletedinuse: 389
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 *** allocated 1946160 integers for termspace/termends
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 599253
% 226.47/226.91 Kept: 101644
% 226.47/226.91 Inuse: 1304
% 226.47/226.91 Deleted: 40764
% 226.47/226.91 Deletedinuse: 390
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 607943
% 226.47/226.91 Kept: 103661
% 226.47/226.91 Inuse: 1316
% 226.47/226.91 Deleted: 40764
% 226.47/226.91 Deletedinuse: 390
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 621452
% 226.47/226.91 Kept: 105723
% 226.47/226.91 Inuse: 1334
% 226.47/226.91 Deleted: 40764
% 226.47/226.91 Deletedinuse: 390
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 634263
% 226.47/226.91 Kept: 107787
% 226.47/226.91 Inuse: 1349
% 226.47/226.91 Deleted: 40764
% 226.47/226.91 Deletedinuse: 390
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying clauses:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 648003
% 226.47/226.91 Kept: 109788
% 226.47/226.91 Inuse: 1380
% 226.47/226.91 Deleted: 41960
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 658155
% 226.47/226.91 Kept: 112106
% 226.47/226.91 Inuse: 1405
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 669703
% 226.47/226.91 Kept: 114139
% 226.47/226.91 Inuse: 1425
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 *** allocated 9852435 integers for clauses
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 682410
% 226.47/226.91 Kept: 116157
% 226.47/226.91 Inuse: 1440
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 694256
% 226.47/226.91 Kept: 118228
% 226.47/226.91 Inuse: 1454
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 706339
% 226.47/226.91 Kept: 120295
% 226.47/226.91 Inuse: 1470
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 717297
% 226.47/226.91 Kept: 122461
% 226.47/226.91 Inuse: 1489
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 724821
% 226.47/226.91 Kept: 124686
% 226.47/226.91 Inuse: 1499
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 729529
% 226.47/226.91 Kept: 126702
% 226.47/226.91 Inuse: 1506
% 226.47/226.91 Deleted: 41961
% 226.47/226.91 Deletedinuse: 399
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 738377
% 226.47/226.91 Kept: 128733
% 226.47/226.91 Inuse: 1524
% 226.47/226.91 Deleted: 42045
% 226.47/226.91 Deletedinuse: 478
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying clauses:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Intermediate Status:
% 226.47/226.91 Generated: 752236
% 226.47/226.91 Kept: 130992
% 226.47/226.91 Inuse: 1532
% 226.47/226.91 Deleted: 51869
% 226.47/226.91 Deletedinuse: 508
% 226.47/226.91
% 226.47/226.91 Resimplifying inuse:
% 226.47/226.91 Done
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Bliksems!, er is een bewijs:
% 226.47/226.91 % SZS status Theorem
% 226.47/226.91 % SZS output start Refutation
% 226.47/226.91
% 226.47/226.91 (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 226.47/226.91 , aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.91 (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 226.47/226.91 , sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 (7) {G0,W17,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y )
% 226.47/226.91 , ! aNaturalNumber0( Z ), sdtpldt0( X, sdtpldt0( Y, Z ) ) ==> sdtpldt0(
% 226.47/226.91 sdtpldt0( X, Y ), Z ) }.
% 226.47/226.91 (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 226.47/226.91 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y = Z
% 226.47/226.91 }.
% 226.47/226.91 (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), ! aNaturalNumber0( Y
% 226.47/226.91 ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 226.47/226.91 }.
% 226.47/226.91 (36) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 226.47/226.91 (37) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 226.47/226.91 (38) {G0,W3,D2,L1,V0,M1} I { ! xn ==> xl }.
% 226.47/226.91 (39) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol2 ) }.
% 226.47/226.91 (40) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xl, skol2 ) ==> xn }.
% 226.47/226.91 (42) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 226.47/226.91 (44) {G0,W22,D3,L4,V0,M4} I { sdtpldt0( xm, xn ) ==> sdtpldt0( xm, xl ),
% 226.47/226.91 alpha1, sdtpldt0( xn, xm ) ==> sdtpldt0( xl, xm ), ! sdtlseqdt0( sdtpldt0
% 226.47/226.91 ( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (46) {G0,W8,D3,L2,V0,M2} I { ! alpha1, ! sdtlseqdt0( sdtpldt0( xm, xl ),
% 226.47/226.91 sdtpldt0( xm, xn ) ) }.
% 226.47/226.91 (47) {G0,W10,D3,L3,V0,M3} I { aNaturalNumber0( skol3 ), sdtlseqdt0(
% 226.47/226.91 sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.91 (48) {G0,W17,D4,L3,V0,M3} I { sdtpldt0( sdtpldt0( xm, xl ), skol3 ) ==>
% 226.47/226.91 sdtpldt0( xm, xn ), sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) )
% 226.47/226.91 , alpha1 }.
% 226.47/226.91 (84) {G1,W9,D3,L3,V2,M3} Q(27);r(4) { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 226.47/226.91 (102) {G1,W6,D3,L2,V1,M2} R(4,36) { ! aNaturalNumber0( X ), aNaturalNumber0
% 226.47/226.91 ( sdtpldt0( X, xl ) ) }.
% 226.47/226.91 (158) {G1,W9,D3,L2,V1,M2} R(6,36) { ! aNaturalNumber0( X ), sdtpldt0( xl, X
% 226.47/226.91 ) = sdtpldt0( X, xl ) }.
% 226.47/226.91 (159) {G1,W9,D3,L2,V1,M2} R(6,37) { ! aNaturalNumber0( X ), sdtpldt0( xn, X
% 226.47/226.91 ) = sdtpldt0( X, xn ) }.
% 226.47/226.91 (160) {G1,W9,D3,L2,V1,M2} R(6,39) { ! aNaturalNumber0( X ), sdtpldt0( skol2
% 226.47/226.91 , X ) = sdtpldt0( X, skol2 ) }.
% 226.47/226.91 (236) {G1,W13,D4,L3,V1,M3} P(40,7);r(36) { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( skol2 ), sdtpldt0( sdtpldt0( X, xl ), skol2 ) ==>
% 226.47/226.91 sdtpldt0( X, xn ) }.
% 226.47/226.91 (758) {G1,W14,D3,L4,V2,M4} P(18,38);r(37) { ! X = xl, ! aNaturalNumber0( Y
% 226.47/226.91 ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xn ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 (764) {G2,W9,D3,L2,V1,M2} Q(758);r(36) { ! aNaturalNumber0( X ), ! sdtpldt0
% 226.47/226.91 ( X, xn ) ==> sdtpldt0( X, xl ) }.
% 226.47/226.91 (4086) {G1,W19,D3,L5,V2,M5} P(18,46);r(42) { ! alpha1, ! sdtlseqdt0(
% 226.47/226.91 sdtpldt0( X, xl ), sdtpldt0( X, xn ) ), ! aNaturalNumber0( Y ), !
% 226.47/226.91 aNaturalNumber0( X ), ! sdtpldt0( Y, xm ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 (4092) {G1,W10,D3,L3,V0,M3} P(6,46);r(42) { ! alpha1, ! sdtlseqdt0(
% 226.47/226.91 sdtpldt0( xm, xl ), sdtpldt0( xn, xm ) ), ! aNaturalNumber0( xn ) }.
% 226.47/226.91 (5153) {G2,W4,D3,L1,V0,M1} R(102,42) { aNaturalNumber0( sdtpldt0( xm, xl )
% 226.47/226.91 ) }.
% 226.47/226.91 (9847) {G3,W10,D3,L3,V0,M3} P(48,84);f;r(5153) { ! aNaturalNumber0( skol3 )
% 226.47/226.91 , sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.91 (10311) {G4,W8,D3,L2,V0,M2} S(47);r(9847) { sdtlseqdt0( sdtpldt0( xm, xl )
% 226.47/226.91 , sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.91 (21100) {G2,W8,D3,L2,V0,M2} S(4092);r(37) { ! alpha1, ! sdtlseqdt0(
% 226.47/226.91 sdtpldt0( xm, xl ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (21317) {G2,W11,D4,L2,V1,M2} S(236);r(39) { ! aNaturalNumber0( X ),
% 226.47/226.91 sdtpldt0( sdtpldt0( X, xl ), skol2 ) ==> sdtpldt0( X, xn ) }.
% 226.47/226.91 (28648) {G2,W7,D3,L1,V0,M1} R(158,42) { sdtpldt0( xl, xm ) ==> sdtpldt0( xm
% 226.47/226.91 , xl ) }.
% 226.47/226.91 (28912) {G2,W7,D3,L1,V0,M1} R(159,42) { sdtpldt0( xm, xn ) ==> sdtpldt0( xn
% 226.47/226.91 , xm ) }.
% 226.47/226.91 (29112) {G3,W11,D4,L2,V1,M2} R(160,102);d(21317) { ! aNaturalNumber0( X ),
% 226.47/226.91 sdtpldt0( skol2, sdtpldt0( X, xl ) ) ==> sdtpldt0( X, xn ) }.
% 226.47/226.91 (29169) {G2,W7,D3,L2,V1,M2} P(160,84);f;r(39) { ! aNaturalNumber0( X ),
% 226.47/226.91 sdtlseqdt0( X, sdtpldt0( skol2, X ) ) }.
% 226.47/226.91 (29188) {G3,W14,D3,L2,V0,M2} S(44);d(28912);d(28648);d(28648);f;r(21100) {
% 226.47/226.91 sdtpldt0( xn, xm ) ==> sdtpldt0( xm, xl ), ! sdtlseqdt0( sdtpldt0( xm, xl
% 226.47/226.91 ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (42152) {G5,W8,D3,L2,V0,M2} S(10311);d(28912) { alpha1, sdtlseqdt0(
% 226.47/226.91 sdtpldt0( xm, xl ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (94400) {G4,W9,D3,L2,V1,M2} R(29169,102);d(29112) { ! aNaturalNumber0( X )
% 226.47/226.91 , sdtlseqdt0( sdtpldt0( X, xl ), sdtpldt0( X, xn ) ) }.
% 226.47/226.91 (109314) {G5,W12,D3,L4,V2,M4} S(4086);r(94400) { ! alpha1, !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xm ) =
% 226.47/226.91 sdtpldt0( Y, X ) }.
% 226.47/226.91 (109315) {G6,W10,D3,L3,V1,M3} F(109314) { ! alpha1, ! aNaturalNumber0( X )
% 226.47/226.91 , ! sdtpldt0( X, xm ) = sdtpldt0( X, X ) }.
% 226.47/226.91 (109317) {G7,W1,D1,L1,V0,M1} Q(109315);r(42) { ! alpha1 }.
% 226.47/226.91 (130499) {G8,W7,D3,L1,V0,M1} S(42152);r(109317) { sdtlseqdt0( sdtpldt0( xm
% 226.47/226.91 , xl ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (130500) {G9,W7,D3,L1,V0,M1} S(29188);r(130499) { sdtpldt0( xn, xm ) ==>
% 226.47/226.91 sdtpldt0( xm, xl ) }.
% 226.47/226.91 (130514) {G10,W7,D3,L1,V0,M1} S(28912);d(130500) { sdtpldt0( xm, xn ) ==>
% 226.47/226.91 sdtpldt0( xm, xl ) }.
% 226.47/226.91 (132479) {G11,W13,D3,L4,V2,M4} P(18,130514);r(764) { ! aNaturalNumber0( Y )
% 226.47/226.91 , ! aNaturalNumber0( xm ), ! aNaturalNumber0( X ), ! sdtpldt0( Y, xm ) =
% 226.47/226.91 sdtpldt0( Y, X ) }.
% 226.47/226.91 (132481) {G12,W9,D3,L2,V1,M2} F(132479);r(42) { ! aNaturalNumber0( X ), !
% 226.47/226.91 sdtpldt0( X, xm ) = sdtpldt0( X, X ) }.
% 226.47/226.91 (132483) {G13,W0,D0,L0,V0,M0} Q(132481);r(42) { }.
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 % SZS output end Refutation
% 226.47/226.91 found a proof!
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Unprocessed initial clauses:
% 226.47/226.91
% 226.47/226.91 (132485) {G0,W1,D1,L1,V0,M1} { && }.
% 226.47/226.91 (132486) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz00 ) }.
% 226.47/226.91 (132487) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( sz10 ) }.
% 226.47/226.91 (132488) {G0,W3,D2,L1,V0,M1} { ! sz10 = sz00 }.
% 226.47/226.91 (132489) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 226.47/226.91 Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.91 (132490) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0(
% 226.47/226.91 Y ), aNaturalNumber0( sdtasdt0( X, Y ) ) }.
% 226.47/226.91 (132491) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 (132492) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y ), Z ) = sdtpldt0
% 226.47/226.91 ( X, sdtpldt0( Y, Z ) ) }.
% 226.47/226.91 (132493) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0( X, sz00 )
% 226.47/226.91 = X }.
% 226.47/226.91 (132494) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtpldt0( sz00
% 226.47/226.91 , X ) }.
% 226.47/226.91 (132495) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), sdtasdt0( X, Y ) = sdtasdt0( Y, X ) }.
% 226.47/226.91 (132496) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtasdt0( X, Y ), Z ) = sdtasdt0
% 226.47/226.91 ( X, sdtasdt0( Y, Z ) ) }.
% 226.47/226.91 (132497) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz10 )
% 226.47/226.91 = X }.
% 226.47/226.91 (132498) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), X = sdtasdt0( sz10
% 226.47/226.91 , X ) }.
% 226.47/226.91 (132499) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtasdt0( X, sz00 )
% 226.47/226.91 = sz00 }.
% 226.47/226.91 (132500) {G0,W7,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sz00 = sdtasdt0(
% 226.47/226.91 sz00, X ) }.
% 226.47/226.91 (132501) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( X, sdtpldt0( Y, Z ) ) = sdtpldt0
% 226.47/226.91 ( sdtasdt0( X, Y ), sdtasdt0( X, Z ) ) }.
% 226.47/226.91 (132502) {G0,W19,D4,L4,V3,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), sdtasdt0( sdtpldt0( Y, Z ), X ) = sdtpldt0
% 226.47/226.91 ( sdtasdt0( Y, X ), sdtasdt0( Z, X ) ) }.
% 226.47/226.91 (132503) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) = sdtpldt0( X, Z ), Y =
% 226.47/226.91 Z }.
% 226.47/226.91 (132504) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( Y, X ) = sdtpldt0( Z, X ), Y =
% 226.47/226.91 Z }.
% 226.47/226.91 (132505) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( X, Y ) =
% 226.47/226.91 sdtasdt0( X, Z ), Y = Z }.
% 226.47/226.91 (132506) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), X = sz00, !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtasdt0( Y, X ) =
% 226.47/226.91 sdtasdt0( Z, X ), Y = Z }.
% 226.47/226.91 (132507) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtpldt0( X, Y ) = sz00, X = sz00 }.
% 226.47/226.91 (132508) {G0,W12,D3,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtpldt0( X, Y ) = sz00, Y = sz00 }.
% 226.47/226.91 (132509) {G0,W15,D3,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtasdt0( X, Y ) = sz00, X = sz00, Y = sz00 }.
% 226.47/226.91 (132510) {G0,W11,D3,L4,V4,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), aNaturalNumber0( skol1( Z, T ) ) }.
% 226.47/226.91 (132511) {G0,W14,D4,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), sdtpldt0( X, skol1( X, Y ) ) = Y }.
% 226.47/226.91 (132512) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y, sdtlseqdt0( X, Y )
% 226.47/226.91 }.
% 226.47/226.91 (132513) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), aNaturalNumber0( Z )
% 226.47/226.91 }.
% 226.47/226.91 (132514) {G0,W17,D3,L5,V3,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), ! Z = sdtmndt0( Y, X ), sdtpldt0( X, Z ) = Y
% 226.47/226.91 }.
% 226.47/226.91 (132515) {G0,W19,D3,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) =
% 226.47/226.91 Y, Z = sdtmndt0( Y, X ) }.
% 226.47/226.91 (132516) {G0,W5,D2,L2,V1,M2} { ! aNaturalNumber0( X ), sdtlseqdt0( X, X )
% 226.47/226.91 }.
% 226.47/226.91 (132517) {G0,W13,D2,L5,V2,M5} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, X ), X = Y }.
% 226.47/226.91 (132518) {G0,W15,D2,L6,V3,M6} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), ! aNaturalNumber0( Z ), ! sdtlseqdt0( X, Y ), ! sdtlseqdt0( Y, Z )
% 226.47/226.91 , sdtlseqdt0( X, Z ) }.
% 226.47/226.91 (132519) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), sdtlseqdt0( X, Y ), ! Y = X }.
% 226.47/226.91 (132520) {G0,W10,D2,L4,V2,M4} { ! aNaturalNumber0( X ), ! aNaturalNumber0
% 226.47/226.91 ( Y ), sdtlseqdt0( X, Y ), sdtlseqdt0( Y, X ) }.
% 226.47/226.91 (132521) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 226.47/226.91 (132522) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 226.47/226.91 (132523) {G0,W3,D2,L1,V0,M1} { ! xl = xn }.
% 226.47/226.91 (132524) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol2 ) }.
% 226.47/226.91 (132525) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xl, skol2 ) = xn }.
% 226.47/226.91 (132526) {G0,W3,D2,L1,V0,M1} { sdtlseqdt0( xl, xn ) }.
% 226.47/226.91 (132527) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 226.47/226.91 (132528) {G0,W26,D4,L5,V1,M5} { sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ),
% 226.47/226.91 alpha1, sdtpldt0( xl, xm ) = sdtpldt0( xn, xm ), ! aNaturalNumber0( X ),
% 226.47/226.91 ! sdtpldt0( sdtpldt0( xl, xm ), X ) = sdtpldt0( xn, xm ) }.
% 226.47/226.91 (132529) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ),
% 226.47/226.91 alpha1, sdtpldt0( xl, xm ) = sdtpldt0( xn, xm ), ! sdtlseqdt0( sdtpldt0(
% 226.47/226.91 xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.91 (132530) {G0,W12,D4,L3,V1,M3} { ! alpha1, ! aNaturalNumber0( X ), !
% 226.47/226.91 sdtpldt0( sdtpldt0( xm, xl ), X ) = sdtpldt0( xm, xn ) }.
% 226.47/226.91 (132531) {G0,W8,D3,L2,V0,M2} { ! alpha1, ! sdtlseqdt0( sdtpldt0( xm, xl )
% 226.47/226.91 , sdtpldt0( xm, xn ) ) }.
% 226.47/226.91 (132532) {G0,W10,D3,L3,V0,M3} { aNaturalNumber0( skol3 ), sdtlseqdt0(
% 226.47/226.91 sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.91 (132533) {G0,W17,D4,L3,V0,M3} { sdtpldt0( sdtpldt0( xm, xl ), skol3 ) =
% 226.47/226.91 sdtpldt0( xm, xn ), sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) )
% 226.47/226.91 , alpha1 }.
% 226.47/226.91
% 226.47/226.91
% 226.47/226.91 Total Proof:
% 226.47/226.91
% 226.47/226.91 subsumption: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.91 parent0: (132489) {G0,W8,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 1 ==> 1
% 226.47/226.91 2 ==> 2
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 parent0: (132491) {G0,W11,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 1 ==> 1
% 226.47/226.91 2 ==> 2
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 eqswap: (132544) {G0,W17,D4,L4,V3,M4} { sdtpldt0( X, sdtpldt0( Y, Z ) ) =
% 226.47/226.91 sdtpldt0( sdtpldt0( X, Y ), Z ), ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 226.47/226.91 parent0[3]: (132492) {G0,W17,D4,L4,V3,M4} { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtpldt0( sdtpldt0( X, Y )
% 226.47/226.91 , Z ) = sdtpldt0( X, sdtpldt0( Y, Z ) ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 Z := Z
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (7) {G0,W17,D4,L4,V3,M4} I { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), sdtpldt0( X, sdtpldt0( Y, Z
% 226.47/226.91 ) ) ==> sdtpldt0( sdtpldt0( X, Y ), Z ) }.
% 226.47/226.91 parent0: (132544) {G0,W17,D4,L4,V3,M4} { sdtpldt0( X, sdtpldt0( Y, Z ) ) =
% 226.47/226.91 sdtpldt0( sdtpldt0( X, Y ), Z ), ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 Z := Z
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 3
% 226.47/226.91 1 ==> 0
% 226.47/226.91 2 ==> 1
% 226.47/226.91 3 ==> 2
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (18) {G0,W16,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 226.47/226.91 sdtpldt0( X, Z ), Y = Z }.
% 226.47/226.91 parent0: (132503) {G0,W16,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Y ) =
% 226.47/226.91 sdtpldt0( X, Z ), Y = Z }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 Z := Z
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 1 ==> 1
% 226.47/226.91 2 ==> 2
% 226.47/226.91 3 ==> 3
% 226.47/226.91 4 ==> 4
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 226.47/226.91 sdtlseqdt0( X, Y ) }.
% 226.47/226.91 parent0: (132512) {G0,W14,D3,L5,V3,M5} { ! aNaturalNumber0( X ), !
% 226.47/226.91 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 226.47/226.91 sdtlseqdt0( X, Y ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 X := X
% 226.47/226.91 Y := Y
% 226.47/226.91 Z := Z
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 1 ==> 1
% 226.47/226.91 2 ==> 2
% 226.47/226.91 3 ==> 3
% 226.47/226.91 4 ==> 4
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (36) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 226.47/226.91 parent0: (132521) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xl ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 subsumption: (37) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 226.47/226.91 parent0: (132522) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xn ) }.
% 226.47/226.91 substitution0:
% 226.47/226.91 end
% 226.47/226.91 permutation0:
% 226.47/226.91 0 ==> 0
% 226.47/226.91 end
% 226.47/226.91
% 226.47/226.91 eqswap: (133356) {G0,W3,D2,L1,V0,M1} { ! xn = xl }.
% 226.47/226.91 parent0[0]: (132523) {G0,W3,D2,L1,V0,M1} { ! xl = xn }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (38) {G0,W3,D2,L1,V0,M1} I { ! xn ==> xl }.
% 226.47/226.92 parent0: (133356) {G0,W3,D2,L1,V0,M1} { ! xn = xl }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (39) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol2 ) }.
% 226.47/226.92 parent0: (132524) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( skol2 ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (40) {G0,W5,D3,L1,V0,M1} I { sdtpldt0( xl, skol2 ) ==> xn }.
% 226.47/226.92 parent0: (132525) {G0,W5,D3,L1,V0,M1} { sdtpldt0( xl, skol2 ) = xn }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (42) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xm ) }.
% 226.47/226.92 parent0: (132527) {G0,W2,D2,L1,V0,M1} { aNaturalNumber0( xm ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 eqswap: (134164) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xn, xm ) = sdtpldt0( xl
% 226.47/226.92 , xm ), sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ), alpha1, ! sdtlseqdt0(
% 226.47/226.92 sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 parent0[2]: (132529) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xm, xl ) = sdtpldt0
% 226.47/226.92 ( xm, xn ), alpha1, sdtpldt0( xl, xm ) = sdtpldt0( xn, xm ), ! sdtlseqdt0
% 226.47/226.92 ( sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 eqswap: (134165) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xm, xn ) = sdtpldt0( xm
% 226.47/226.92 , xl ), sdtpldt0( xn, xm ) = sdtpldt0( xl, xm ), alpha1, ! sdtlseqdt0(
% 226.47/226.92 sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 parent0[1]: (134164) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xn, xm ) = sdtpldt0
% 226.47/226.92 ( xl, xm ), sdtpldt0( xm, xl ) = sdtpldt0( xm, xn ), alpha1, ! sdtlseqdt0
% 226.47/226.92 ( sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (44) {G0,W22,D3,L4,V0,M4} I { sdtpldt0( xm, xn ) ==> sdtpldt0
% 226.47/226.92 ( xm, xl ), alpha1, sdtpldt0( xn, xm ) ==> sdtpldt0( xl, xm ), !
% 226.47/226.92 sdtlseqdt0( sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 parent0: (134165) {G0,W22,D3,L4,V0,M4} { sdtpldt0( xm, xn ) = sdtpldt0( xm
% 226.47/226.92 , xl ), sdtpldt0( xn, xm ) = sdtpldt0( xl, xm ), alpha1, ! sdtlseqdt0(
% 226.47/226.92 sdtpldt0( xl, xm ), sdtpldt0( xn, xm ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 2
% 226.47/226.92 2 ==> 1
% 226.47/226.92 3 ==> 3
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (46) {G0,W8,D3,L2,V0,M2} I { ! alpha1, ! sdtlseqdt0( sdtpldt0
% 226.47/226.92 ( xm, xl ), sdtpldt0( xm, xn ) ) }.
% 226.47/226.92 parent0: (132531) {G0,W8,D3,L2,V0,M2} { ! alpha1, ! sdtlseqdt0( sdtpldt0(
% 226.47/226.92 xm, xl ), sdtpldt0( xm, xn ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (47) {G0,W10,D3,L3,V0,M3} I { aNaturalNumber0( skol3 ),
% 226.47/226.92 sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.92 parent0: (132532) {G0,W10,D3,L3,V0,M3} { aNaturalNumber0( skol3 ),
% 226.47/226.92 sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0( xm, xn ) ), alpha1 }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 2 ==> 2
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (48) {G0,W17,D4,L3,V0,M3} I { sdtpldt0( sdtpldt0( xm, xl ),
% 226.47/226.92 skol3 ) ==> sdtpldt0( xm, xn ), sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0
% 226.47/226.92 ( xm, xn ) ), alpha1 }.
% 226.47/226.92 parent0: (132533) {G0,W17,D4,L3,V0,M3} { sdtpldt0( sdtpldt0( xm, xl ),
% 226.47/226.92 skol3 ) = sdtpldt0( xm, xn ), sdtlseqdt0( sdtpldt0( xm, xl ), sdtpldt0(
% 226.47/226.92 xm, xn ) ), alpha1 }.
% 226.47/226.92 substitution0:
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 2 ==> 2
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 eqswap: (134800) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 226.47/226.92 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 226.47/226.92 sdtlseqdt0( X, Z ) }.
% 226.47/226.92 parent0[3]: (27) {G0,W14,D3,L5,V3,M5} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), ! aNaturalNumber0( Z ), ! sdtpldt0( X, Z ) = Y,
% 226.47/226.92 sdtlseqdt0( X, Y ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Z
% 226.47/226.92 Z := Y
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 eqrefl: (134801) {G0,W13,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( sdtpldt0( X, Y ) ), ! aNaturalNumber0( Y ), sdtlseqdt0(
% 226.47/226.92 X, sdtpldt0( X, Y ) ) }.
% 226.47/226.92 parent0[0]: (134800) {G0,W14,D3,L5,V3,M5} { ! Z = sdtpldt0( X, Y ), !
% 226.47/226.92 aNaturalNumber0( X ), ! aNaturalNumber0( Z ), ! aNaturalNumber0( Y ),
% 226.47/226.92 sdtlseqdt0( X, Z ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 Z := sdtpldt0( X, Y )
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 resolution: (134806) {G1,W13,D3,L5,V2,M5} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 226.47/226.92 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 226.47/226.92 parent0[1]: (134801) {G0,W13,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( sdtpldt0( X, Y ) ), ! aNaturalNumber0( Y ), sdtlseqdt0(
% 226.47/226.92 X, sdtpldt0( X, Y ) ) }.
% 226.47/226.92 parent1[2]: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 end
% 226.47/226.92 substitution1:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 factor: (134808) {G1,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 226.47/226.92 aNaturalNumber0( Y ) }.
% 226.47/226.92 parent0[0, 3]: (134806) {G1,W13,D3,L5,V2,M5} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 226.47/226.92 aNaturalNumber0( X ), ! aNaturalNumber0( Y ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 factor: (134810) {G1,W9,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 226.47/226.92 parent0[1, 3]: (134808) {G1,W11,D3,L4,V2,M4} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ), !
% 226.47/226.92 aNaturalNumber0( Y ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (84) {G1,W9,D3,L3,V2,M3} Q(27);r(4) { ! aNaturalNumber0( X ),
% 226.47/226.92 ! aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 226.47/226.92 parent0: (134810) {G1,W9,D3,L3,V2,M3} { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtlseqdt0( X, sdtpldt0( X, Y ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := Y
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 2 ==> 2
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 resolution: (134813) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 226.47/226.92 aNaturalNumber0( sdtpldt0( X, xl ) ) }.
% 226.47/226.92 parent0[1]: (4) {G0,W8,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), aNaturalNumber0( sdtpldt0( X, Y ) ) }.
% 226.47/226.92 parent1[0]: (36) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 Y := xl
% 226.47/226.92 end
% 226.47/226.92 substitution1:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (102) {G1,W6,D3,L2,V1,M2} R(4,36) { ! aNaturalNumber0( X ),
% 226.47/226.92 aNaturalNumber0( sdtpldt0( X, xl ) ) }.
% 226.47/226.92 parent0: (134813) {G1,W6,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 226.47/226.92 aNaturalNumber0( sdtpldt0( X, xl ) ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 resolution: (134814) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( xl, X ) = sdtpldt0( X, xl ) }.
% 226.47/226.92 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.92 parent1[0]: (36) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xl ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := xl
% 226.47/226.92 Y := X
% 226.47/226.92 end
% 226.47/226.92 substitution1:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (158) {G1,W9,D3,L2,V1,M2} R(6,36) { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( xl, X ) = sdtpldt0( X, xl ) }.
% 226.47/226.92 parent0: (134814) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0(
% 226.47/226.92 xl, X ) = sdtpldt0( X, xl ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 resolution: (134816) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( xn, X ) = sdtpldt0( X, xn ) }.
% 226.47/226.92 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.92 parent1[0]: (37) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( xn ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := xn
% 226.47/226.92 Y := X
% 226.47/226.92 end
% 226.47/226.92 substitution1:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (159) {G1,W9,D3,L2,V1,M2} R(6,37) { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( xn, X ) = sdtpldt0( X, xn ) }.
% 226.47/226.92 parent0: (134816) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0(
% 226.47/226.92 xn, X ) = sdtpldt0( X, xn ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := X
% 226.47/226.92 end
% 226.47/226.92 permutation0:
% 226.47/226.92 0 ==> 0
% 226.47/226.92 1 ==> 1
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 resolution: (134818) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( skol2, X ) = sdtpldt0( X, skol2 ) }.
% 226.47/226.92 parent0[0]: (6) {G0,W11,D3,L3,V2,M3} I { ! aNaturalNumber0( X ), !
% 226.47/226.92 aNaturalNumber0( Y ), sdtpldt0( X, Y ) = sdtpldt0( Y, X ) }.
% 226.47/226.92 parent1[0]: (39) {G0,W2,D2,L1,V0,M1} I { aNaturalNumber0( skol2 ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := skol2
% 226.47/226.92 Y := X
% 226.47/226.92 end
% 226.47/226.92 substitution1:
% 226.47/226.92 end
% 226.47/226.92
% 226.47/226.92 subsumption: (160) {G1,W9,D3,L2,V1,M2} R(6,39) { ! aNaturalNumber0( X ),
% 226.47/226.92 sdtpldt0( skol2, X ) = sdtpldt0( X, skol2 ) }.
% 226.47/226.92 parent0: (134818) {G1,W9,D3,L2,V1,M2} { ! aNaturalNumber0( X ), sdtpldt0(
% 226.47/226.92 skol2, X ) = sdtpldt0( X, skol2 ) }.
% 226.47/226.92 substitution0:
% 226.47/226.92 X := Cputime limit exceeded (core dumped)
%------------------------------------------------------------------------------